cfarm.tetaneutral.net - Compile Farm

Stream: general

[Kenny Lau]

@Tobias Grosser I have an account now. How do I use it?

[Johan Commelin]

@Tobias Grosser I have an account now. How do I use it?

We need a Would-you-please-move-this-to-another-thread-Thank-you-emoji

[Reid Barton]

Looks like the instructions are at https://cfarm.tetaneutral.net/machines/list/, just ssh into one of the machines

[Kenny Lau]

it requires a password and I don't know where to get the password from

[Reid Barton]

Oh, uh... hmm. I would assume you're supposed to use ssh certificates but I also don't see how to set that up

[Reid Barton]

I just requested an account a minute or two ago, so I don't know.
I see there is a Login link in the top right of the web page though

[Tobias Grosser]

@Johan Commelin, indeed. Sorry for this distraction.

[Tobias Grosser]

I use my ssh key to login. Not sure how this is handled today, but either you should have had a way to specify a password when registering or an ssh key, I assume.

[Tobias Grosser]

The website states: Once your account is created, you will be able to upload SSH keys and gain SSH access to all machines of the platform.

[Tobias Grosser]

So seems you need to wait until your account is confirmed.

[Reid Barton]

I have an account now and I uploaded an SSH public key using the web interface but it takes some time for the key to be propagated to the machines. Kenny are you in the same situation?

[Kenny Lau]

I have no idea what SSH is

[Kenny Lau]

what do you mean by upload an SSH public key

[Bryan Gin-ge Chen]

You'll want to do something like this https://help.github.com/articles/generating-a-new-ssh-key-and-adding-it-to-the-ssh-agent/#platform-windows

[Reid Barton]

Yes, then you can use the cfarm web interface to add the ssh key to your account

[Johan Commelin]

@Johan Commelin, indeed. Sorry for this distraction.

No worries (-;

[Kenny Lau]

So what do I do when they ask me for the password?

[Scott Morrison]

Upload an ssh key, so it doesn't ask you for a password?

[Kenny Lau]

it's still asking me for a password

[Kenny Lau]

and 1.5 hour has already passed

[Reid Barton]

I had to wait at least several hours (haven't tried to log in today)

[Reid Barton]

I can now log in. Time to see if I can build lean on a POWER8 system

[Reid Barton]

ok, got this working now... 2406 is the CPU% column

 31366 rwbarton  20   0 10.851g 3.304g  15872 S  2406  1.3  50:19.98 lean

[Reid Barton]

The big sparc machine had unsatisfactory results--the release version of lean crashed, and the debug version mostly doesn't crash, but building mathlib did trigger some assertion and is super slow.

LEAN ASSERTION VIOLATION
File: /home/rwbarton/lean/lean/src/library/type_context.cpp
Line: 1230
Task: /home/rwbarton/lean/mathlib2/computability/primrec.lean: primcodable.prod
idx < m_tmp_data->m_uassignment.size()

[Reid Barton]

mathlib on the POWER8 machine:

> lean --make .
28590.38user 105.69system 18:55.94elapsed 2526%CPU (0avgtext+0avgdata 10297280maxresident)k

Pretty parallel but not so good single-threaded performance

[Reid Barton]

Maybe tomorrow I'll try the xeons

[Reid Barton]

Aha, this machine is actually 20 cores with 8-way SMT (IBM equivalent of hyperthreading)

[Reid Barton]

I wonder if that means a well-chosen cpu set would be faster

[Kenny Lau]

@Reid Barton could you teach me how to use it?

[Kenny Lau]

I just connect ssh and then do lean --make?

[Kenny Lau]

how do I make sure I'm using the server's CPU?

[Kenny Lau]

ok I can see that it automatically redirects me to the server

[Kenny Lau]

but now how do I communicate between the server and my computer?

[Johan Commelin]

@Kenny Lau What kind of communication do you want?

[Johan Commelin]

You can copy files

[Kenny Lau]

how?

[Johan Commelin]

scp

[Johan Commelin]

It uses ssh

[Johan Commelin]

But what do you want to copy?

[Johan Commelin]

Can't you just git clone on that server?

[Kenny Lau]

then how do I send the olean files back?

[Johan Commelin]

Aah, from the server to your box?

[Kenny Lau]

both ways

[Johan Commelin]

Both times scp on your box

[Kenny Lau]

how to use scp?

[Johan Commelin]

scp my_file.olean server:~/destination.olean

[Johan Commelin]

scp -r server:~/a_directory/ my_directory/ ## recursive

[Kenny Lau]

what is -R?

[Johan Commelin]

Sorry, should be -r.

[Johan Commelin]

scp can also be used as scp server1:path1 server2:path2. It's pretty general (-;

[Johan Commelin]

I guess there are ways to recurse and only copy olean files.

[Johan Commelin]

Maybe rsync can help. It will also use your ssh keys.

[Johan Commelin]

@Kenny Lau What OS are you on?

[Kenny Lau]

windows

[Johan Commelin]

/me shuts his eyes while Tux :penguin: slaps Kenny in the face.

[Johan Commelin]

@Kenny Lau I'm not sure if rsync is available. Can you try if it is?

[Kenny Lau]

it is

[Johan Commelin]

You're lucky (-;

[Kenny Lau]

I'm using something that has the unix commands

[Johan Commelin]

Do you know man?

[Kenny Lau]

oh no scp is copying the files one by one

[Kenny Lau]

it will take years

[Johan Commelin]

Ctrl-C

[Johan Commelin]

Also try man man.

[Kenny Lau]

so how do I even use this if I can't copy the files

[Johan Commelin]

Did you try man man?

[Kenny Lau]

yes

[Johan Commelin]

What happened?

[Kenny Lau]

i get a long manual?

[Johan Commelin]

Great. Try man rsync

[Kenny Lau]

how do I refer to my computer from the server?

[Johan Commelin]

That's harder.

[Kenny Lau]

:(

[Johan Commelin]

You can setup a reverse tunnel using ssh

[Johan Commelin]

See man ssh

[Johan Commelin]

But why would you want that?

[Kenny Lau]

I don't have rsync, but the server has rsync

[Johan Commelin]

Aah, to use rsync the other side needs some form of an ssh server I think. So that won't help you.

[Johan Commelin]

A better solution would be to install rsync locally.

[Kenny Lau]

how do I do that?

[Johan Commelin]

I dunno. Haven't touched windows in 15 years.

[Kenny Lau]

just treat me as using bash

[Johan Commelin]

You know that the latest Total War series also runs on Linux?

[Kenny Lau]

ok so I rsynced lean and mathlib, but now I can't run lean.exe

[Andrew Ashworth]

You won't be able to do what you want with a Windows host machine

[Andrew Ashworth]

Oleans aren't compatible between operating systems

[Kevin Buzzard]

exes are certainly not compatible between operating systems

[Kenny Lau]

this is so sad

[Johan Commelin]

Right. Please blame Bill Gates.

[Kenny Lau]

so then how do you install lean on linux?

[Johan Commelin]

@Kenny Lau Would you mind explaining the bigger goal that you have in mind with this service?

[Johan Commelin]

Also is X installed on that server, can you do ssh with X forwarding? If so, just install VScode, and run it on the server. The rest is history.

[Johan Commelin]

But I guess that you can't have X forwarding.

[Kenny Lau]

well with this service I can test the compile times quicklier

[Johan Commelin]

Have you looked at the travis config?

[Johan Commelin]

For mathlib on github

[Johan Commelin]

It will tell Travis how to compile mathlib. I guess it could also tell you how to use this server

[Johan Commelin]

https://github.com/leanprover/mathlib/blob/master/.travis.yml

[Kenny Lau]

[kc_kennylau@gcc2-power8 ~]$ curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
info: downloading installer
curl: (22) The requested URL returned error: 404 Not Found
elan: command failed: curl -sSfL https://github.com/Kha/elan/releases/download/v0.7.1/elan-powerpc64le-unknown-linux-gnu.tar.gz -o /tmp/tmp.Yt4psW5eYO/elan-init.tar.gz

[Johan Commelin]

which wget

[Johan Commelin]

Oh nvm

[Johan Commelin]

I didn't read the error

[Johan Commelin]

That elan command is asking curl to write something to /tmp/. Maybe you don't have permissions there?

[Johan Commelin]

But curl is also getting a 404

[Johan Commelin]

Before that

[Kenny Lau]

then how did Tobias Grosser manage to do it

[Johan Commelin]

This explains why: https://github.com/Kha/elan/releases/

[Johan Commelin]

You are on a powerpc

[Johan Commelin]

That architecture is not supported by elan.

[Johan Commelin]

@Tobias Grosser Can you tell how you did this?

[Tobias Grosser]

I did not get anything running on powerpc

[Tobias Grosser]

$ssh gcc20.fsffrance.org

[Tobias Grosser]

In fact, I did not use the compilefarm to compile lean.

[Tobias Grosser]

I would start with gcc20.fsffrance.org

[Tobias Grosser]

The easiest is probably to create a linux docker image with a current lean environment.

[Tobias Grosser]

And then use udocker to run it.

[Tobias Grosser]

Also, I am not sure kenny why you want to copy files.

[Kenny Lau]

ignore the part about copying files

[Tobias Grosser]

OK.

[Tobias Grosser]

In theory you should be able to just run:

[Tobias Grosser]

grosser@gcc20:~$ curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
info: downloading installer

/tmp/tmp.OXhfu8gCPt/elan-init: /lib/x86_64-linux-gnu/libc.so.6: version GLIBC_2.15' not found (required by /tmp/tmp.OXhfu8gCPt/elan-init) /tmp/tmp.OXhfu8gCPt/elan-init: /lib/x86_64-linux-gnu/libc.so.6: version GLIBC_2.14' not found (required by /tmp/tmp.OXhfu8gCPt/elan-init)
grosser@gcc20:~$

[Tobias Grosser]

Unfortunately this gives an error

[Tobias Grosser]

As the glibc version is not correct.

[Tobias Grosser]

What you can do instead on gcc20:

curl https://raw.githubusercontent.com/indigo-dc/udocker/master/udocker.py > udocker
chmod u+rx ./udocker
./udocker install
./udocker pull ubuntu
./udocker create --name=lean ubuntu
./udocker run lean
apt-get update
apt-get install curl git
curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
 git clone https://github.com/leanprover/mathlib.git
leanpkg --make

to get back into your lean folder just run

./udocker run lean
cd mathlib
ls

[Reid Barton]

I feel obliged to point out that copying build results from the farm machines isn't good practice in terms of security, even if the risks are low for olean files. Better to only copy things to the farm machines.

[Reid Barton]

I would suggest using the machines gcc120-gcc123, I got 10 minutes mathlib build time on gcc120 and elan worked without any issues. Note they are on nonstandard ports (45000 through 45003 respectively)

[Reid Barton]

Though Scott's machine is still the leader at 8 minutes.

[Tobias Grosser]

@Reid Barton, this seems to be a great idea.

[Tobias Grosser]

Did not see gcc120ff

[Kenny Lau]

I did curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh and it said elan has been installed when in fact it hasn't been.

[Kenny Lau]

and I thus can't install elan.

[Kenny Lau]

I tried on both gcc120 port 45000 and gcc121 port 45001

[Reid Barton]

Did you do the step printed out at the end of the elan output, i.e., source <something>?

[Reid Barton]

Or log out and log back in

[Kenny Lau]

[kc_kennylau@gcc120 ~]$ curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh
info: downloading installer

Welcome to Lean!

This will download and install Elan, a tool for managing different Lean
versions used in packages you create or download. It will also install a
default version of Lean and its package manager, leanpkg, for editing files not
belonging to any package.

It will add the leanpkg, lean, and elan commands to Elan's bin directory,
located at:

  /home/kc_kennylau/.elan/bin

This path will then be added to your PATH environment variable by modifying the
profile files located at:

  /home/kc_kennylau/.profile
  /home/kc_kennylau/.bash_profile

You can uninstall at any time with elan self uninstall and these changes will
be reverted.

Current installation options:

     default toolchain: stable
  modify PATH variable: yes

1) Proceed with installation (default)
2) Customize installation
3) Cancel installation
1

info: updating existing elan installation


Elan is installed now. Great!

To get started you need Elan's bin directory ($HOME/.elan/bin) in your PATH
environment variable. Next time you log in this will be done automatically.

To configure your current shell run source $HOME/.elan/env
[kc_kennylau@gcc120 ~]$ source $HOME/.lean/env
-bash: /home/kc_kennylau/.lean/env: No such file or directory

[Reid Barton]

Hmm, that is odd. It worked for me

[Kenny Lau]

i'm on windows using msys2 mingw 64, if that makes any difference

[Reid Barton]

Wait no! you typed it wrong

[Reid Barton]

.elan not .lean

[Kenny Lau]

I'm stupid.

[Kenny Lau]

it worked now

[Mario Carneiro]

I wonder who thought naming the downloader for lean an anagram of lean was a good idea :P

[Reid Barton]

Maybe they should have chosen a less easily confused name, like rustup

[Mario Carneiro]

you want the downloader for lean to be called rustup? That's indeed less easily confused with lean