Zulip Chat Archive

Stream: general

Topic: cfarm.tetaneutral.net - Compile Farm


view this post on Zulip Kenny Lau (Oct 09 2018 at 18:43):

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

view this post on Zulip Johan Commelin (Oct 09 2018 at 18:48):

@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

view this post on Zulip Reid Barton (Oct 09 2018 at 19:04):

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

view this post on Zulip Kenny Lau (Oct 09 2018 at 19:05):

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

view this post on Zulip Reid Barton (Oct 09 2018 at 19:06):

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

view this post on Zulip Reid Barton (Oct 09 2018 at 19:07):

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

view this post on Zulip Tobias Grosser (Oct 09 2018 at 20:37):

@Johan Commelin, indeed. Sorry for this distraction.

view this post on Zulip Tobias Grosser (Oct 09 2018 at 20:39):

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.

view this post on Zulip Tobias Grosser (Oct 09 2018 at 20:40):

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.

view this post on Zulip Tobias Grosser (Oct 09 2018 at 20:40):

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

view this post on Zulip Reid Barton (Oct 09 2018 at 22:35):

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?

view this post on Zulip Kenny Lau (Oct 09 2018 at 22:41):

I have no idea what SSH is

view this post on Zulip Kenny Lau (Oct 09 2018 at 22:41):

what do you mean by upload an SSH public key

view this post on Zulip Bryan Gin-ge Chen (Oct 09 2018 at 22:46):

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

view this post on Zulip Reid Barton (Oct 09 2018 at 23:04):

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

view this post on Zulip Johan Commelin (Oct 10 2018 at 01:20):

@Johan Commelin, indeed. Sorry for this distraction.

No worries (-;

view this post on Zulip Kenny Lau (Oct 10 2018 at 20:44):

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

view this post on Zulip Scott Morrison (Oct 10 2018 at 22:09):

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

view this post on Zulip Kenny Lau (Oct 10 2018 at 22:13):

it's still asking me for a password

view this post on Zulip Kenny Lau (Oct 10 2018 at 22:13):

and 1.5 hour has already passed

view this post on Zulip Reid Barton (Oct 10 2018 at 22:21):

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

view this post on Zulip Reid Barton (Oct 11 2018 at 02:16):

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

view this post on Zulip Reid Barton (Oct 11 2018 at 03:49):

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

view this post on Zulip Reid Barton (Oct 11 2018 at 03:50):

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()

view this post on Zulip Reid Barton (Oct 11 2018 at 04:07):

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

view this post on Zulip Reid Barton (Oct 11 2018 at 04:07):

Maybe tomorrow I'll try the xeons

view this post on Zulip Reid Barton (Oct 11 2018 at 04:19):

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

view this post on Zulip Reid Barton (Oct 11 2018 at 04:20):

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

view this post on Zulip Kenny Lau (Oct 11 2018 at 08:53):

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

view this post on Zulip Kenny Lau (Oct 11 2018 at 08:53):

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

view this post on Zulip Kenny Lau (Oct 11 2018 at 08:53):

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

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:11):

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

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:11):

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

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:12):

@Kenny Lau What kind of communication do you want?

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:12):

You can copy files

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:12):

how?

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:12):

scp

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:12):

It uses ssh

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:12):

But what do you want to copy?

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:12):

Can't you just git clone on that server?

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:13):

then how do I send the olean files back?

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:13):

Aah, from the server to your box?

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:13):

both ways

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:13):

Both times scp on your box

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:13):

how to use scp?

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:14):

scp my_file.olean server:~/destination.olean

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:14):

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

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:15):

what is -R?

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:15):

Sorry, should be -r.

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:15):

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

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:16):

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

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:16):

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

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:16):

@Kenny Lau What OS are you on?

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:16):

windows

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:17):

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

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:18):

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

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:18):

it is

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:18):

You're lucky (-;

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:18):

I'm using something that has the unix commands

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:20):

Do you know man?

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:21):

oh no scp is copying the files one by one

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:21):

it will take years

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:21):

Ctrl-C

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:21):

Also try man man.

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:22):

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

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:22):

Did you try man man?

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:22):

yes

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:23):

What happened?

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:23):

i get a long manual?

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:23):

Great. Try man rsync

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:24):

how do I refer to my computer from the server?

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:24):

That's harder.

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:24):

:(

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:24):

You can setup a reverse tunnel using ssh

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:25):

See man ssh

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:25):

But why would you want that?

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:25):

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

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:26):

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

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:26):

A better solution would be to install rsync locally.

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:27):

how do I do that?

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:27):

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

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:27):

just treat me as using bash

view this post on Zulip Johan Commelin (Oct 11 2018 at 09:27):

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

view this post on Zulip Kenny Lau (Oct 11 2018 at 09:57):

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

view this post on Zulip Andrew Ashworth (Oct 11 2018 at 10:31):

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

view this post on Zulip Andrew Ashworth (Oct 11 2018 at 10:31):

Oleans aren't compatible between operating systems

view this post on Zulip Kevin Buzzard (Oct 11 2018 at 12:47):

exes are certainly not compatible between operating systems

view this post on Zulip Kenny Lau (Oct 11 2018 at 14:10):

this is so sad

view this post on Zulip Johan Commelin (Oct 11 2018 at 14:11):

Right. Please blame Bill Gates.

view this post on Zulip Kenny Lau (Oct 11 2018 at 14:16):

so then how do you install lean on linux?

view this post on Zulip Johan Commelin (Oct 11 2018 at 14:18):

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

view this post on Zulip Johan Commelin (Oct 11 2018 at 14:19):

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.

view this post on Zulip Johan Commelin (Oct 11 2018 at 14:19):

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

view this post on Zulip Kenny Lau (Oct 11 2018 at 14:19):

well with this service I can test the compile times quicklier

view this post on Zulip Johan Commelin (Oct 11 2018 at 14:22):

Have you looked at the travis config?

view this post on Zulip Johan Commelin (Oct 11 2018 at 14:22):

For mathlib on github

view this post on Zulip Johan Commelin (Oct 11 2018 at 14:22):

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

view this post on Zulip Johan Commelin (Oct 11 2018 at 14:22):

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

view this post on Zulip Kenny Lau (Oct 11 2018 at 14:23):

[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

view this post on Zulip Johan Commelin (Oct 11 2018 at 14:25):

which wget

view this post on Zulip Johan Commelin (Oct 11 2018 at 14:25):

Oh nvm

view this post on Zulip Johan Commelin (Oct 11 2018 at 14:25):

I didn't read the error

view this post on Zulip Johan Commelin (Oct 11 2018 at 14:27):

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

view this post on Zulip Johan Commelin (Oct 11 2018 at 14:27):

But curl is also getting a 404

view this post on Zulip Johan Commelin (Oct 11 2018 at 14:27):

Before that

view this post on Zulip Kenny Lau (Oct 11 2018 at 14:28):

then how did Tobias Grosser manage to do it

view this post on Zulip Johan Commelin (Oct 11 2018 at 14:28):

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

view this post on Zulip Johan Commelin (Oct 11 2018 at 14:28):

You are on a powerpc

view this post on Zulip Johan Commelin (Oct 11 2018 at 14:28):

That architecture is not supported by elan.

view this post on Zulip Johan Commelin (Oct 11 2018 at 14:29):

@Tobias Grosser Can you tell how you did this?

view this post on Zulip Tobias Grosser (Oct 11 2018 at 14:31):

I did not get anything running on powerpc

view this post on Zulip Tobias Grosser (Oct 11 2018 at 14:32):

$ssh gcc20.fsffrance.org

view this post on Zulip Tobias Grosser (Oct 11 2018 at 14:33):

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

view this post on Zulip Tobias Grosser (Oct 11 2018 at 14:33):

I would start with gcc20.fsffrance.org

view this post on Zulip Tobias Grosser (Oct 11 2018 at 14:34):

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

view this post on Zulip Tobias Grosser (Oct 11 2018 at 14:34):

And then use udocker to run it.

view this post on Zulip Tobias Grosser (Oct 11 2018 at 14:34):

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

view this post on Zulip Kenny Lau (Oct 11 2018 at 14:34):

ignore the part about copying files

view this post on Zulip Tobias Grosser (Oct 11 2018 at 14:34):

OK.

view this post on Zulip Tobias Grosser (Oct 11 2018 at 14:34):

In theory you should be able to just run:

view this post on Zulip Tobias Grosser (Oct 11 2018 at 14:34):

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:~$

view this post on Zulip Tobias Grosser (Oct 11 2018 at 14:35):

Unfortunately this gives an error

view this post on Zulip Tobias Grosser (Oct 11 2018 at 14:35):

As the glibc version is not correct.

view this post on Zulip Tobias Grosser (Oct 11 2018 at 14:45):

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

view this post on Zulip Reid Barton (Oct 11 2018 at 14:47):

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.

view this post on Zulip Reid Barton (Oct 11 2018 at 17:54):

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)

view this post on Zulip Reid Barton (Oct 11 2018 at 17:55):

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

view this post on Zulip Tobias Grosser (Oct 11 2018 at 19:05):

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

view this post on Zulip Tobias Grosser (Oct 11 2018 at 19:05):

Did not see gcc120ff

view this post on Zulip Kenny Lau (Oct 11 2018 at 21:44):

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.

view this post on Zulip Kenny Lau (Oct 11 2018 at 21:44):

and I thus can't install elan.

view this post on Zulip Kenny Lau (Oct 11 2018 at 21:45):

I tried on both gcc120 port 45000 and gcc121 port 45001

view this post on Zulip Reid Barton (Oct 11 2018 at 21:46):

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

view this post on Zulip Reid Barton (Oct 11 2018 at 21:46):

Or log out and log back in

view this post on Zulip Kenny Lau (Oct 11 2018 at 22:33):

[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

view this post on Zulip Reid Barton (Oct 11 2018 at 22:34):

Hmm, that is odd. It worked for me

view this post on Zulip Kenny Lau (Oct 11 2018 at 22:34):

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

view this post on Zulip Reid Barton (Oct 11 2018 at 22:35):

Wait no! you typed it wrong

view this post on Zulip Reid Barton (Oct 11 2018 at 22:35):

.elan not .lean

view this post on Zulip Kenny Lau (Oct 11 2018 at 22:36):

I'm stupid.

view this post on Zulip Kenny Lau (Oct 11 2018 at 22:36):

it worked now

view this post on Zulip Mario Carneiro (Oct 11 2018 at 22:37):

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

view this post on Zulip Reid Barton (Oct 11 2018 at 22:37):

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

view this post on Zulip Mario Carneiro (Oct 11 2018 at 22:38):

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


Last updated: May 11 2021 at 12:15 UTC