New user bundles

Stream: general

[Patrick Massot]

I had a first go at automating the build of a bundled autonomous Lean+VScode+mathlib+tutorial (only for Linux at the moment). People interested in this topic can download https://gist.github.com/PatrickMassot/567833153f106379b87a20e9d3a712ef to a Linux box equipped with a recent python together with python packages certifi, urllib3, GitPython, PyGithub (you already have them if you can run update-mathlib). Then run this script. It should build a new folder dist containing an executable file trylean which should launch VScodium running Lean+mathlib on our tutorial file without touching anything outside of /tmp. For those who missed earlier parts of the discussion and wonder what is VScodium, please see https://github.com/VSCodium/vscodium#why.

[Rob Lewis]

This requires Python >= 3.6 I think:

rob@rob-HP-ProDesk-600-G3-MT:~/lean/temp$ python3 mk_bundle.py
  File "mk_bundle.py", line 39
    log.info(f'Searching for {name}')
                                   ^
SyntaxError: invalid syntax
rob@rob-HP-ProDesk-600-G3-MT:~/lean/temp$ python3 --version
Python 3.5.2

[Patrick Massot]

I'm using python 3.8.1

[Patrick Massot]

This is not a script for general users, it's meant to be run by GitHub action.

[Rob Lewis]

Ah. If it were user facing, I'd suggest making it compatible with older Python. But for CI it doesn't matter.

[Patrick Massot]

Sure. But here the goal is to have GitHub producing those bundles, zipping them and put them somewhere beginners can download them. Then the user facing instruction would be:

• if you want to try Lean, download this, unzip, run trylean.
• if you want to become a more serious Lean user, follow https://github.com/leanprover-community/mathlib#installation

[Patrick Massot]

Rob, did you manage to run that script in the end?

[Rob Lewis]

No, doing other things and I didn't look up how to update Python. Will try in a bit.

[Rob Lewis]

After some fussing around with Python versions, this worked great.

[Patrick Massot]

Of course it misses the final zipping action, but this is trivial to add. Do you think we should make variations for Windows and MacOS and ask GitHub actions to run this script after deploy_nightly and push the three resulting zip files somewhere?

[Patrick Massot]

Of course this would also need removing the --pre-release flag I pointed out yesterday.

[Rob Lewis]

Yeah, that can be done. We can publish them as mathlib releases.

[Patrick Massot]

I wouldn't mind if someone who already worked to understand GitHub actions could take over this task.

[Rob Lewis]

If you provide the script that generates the zip files, we can get it into Actions.

[Patrick Massot]

I can do that easily for the Linux version. I'm not sure I can create a zip file that Windows will like from Linux.

[Rob Lewis]

Why not? Is there more to it than changing this line? https://gist.github.com/PatrickMassot/567833153f106379b87a20e9d3a712ef#file-mk_bundle-py-L78

[Patrick Massot]

There a couple more lines to change, it must download the correct binaries of Lean and VScodium.

[Patrick Massot]

But I'll try.

[Patrick Massot]

Ok, I just spend some more time on this newbie bundles thing. I tried the optimistic idea to generate all three platform archive from my linux box. The updated script is at https://gist.github.com/PatrickMassot/567833153f106379b87a20e9d3a712ef. I need people to test the archives from https://www.imo.universite-paris-saclay.fr/~pmassot/try.html. As usual Windows users must be careful to Unblock the zip file before extraction (or extract with 7-zip or some other non-paranoid tool). I'm pretty sure the trylean launcher won't work on MacOS, I need someone who understand macs here (VScode comes as a .app folder, I don't know how to launch that from bash).

[Patrick Massot]

Remember the goal is each archive contains a trylean folder containing everything, and users launch trylean (or trylean.bat on Windows) and start playing immediately.

[Sebastien Gouezel]

Two issues on windows:

• trylean.bat should refer to vscodium and not codium.
• I was hit by https://github.com/VSCodium/vscodium/issues/331. Hopefully this should be fixed in a few days, but for now this makes it unusable.

[Patrick Massot]

Thanks Sébastien! We are really unlucky with Windows paranoia. We'll have to wait a bit (or stick to a VScodium version that works for a while).

[Patrick Massot]

Can anyone try on a Mac?

[Patrick Massot]

@Alex J. Best could you try on your Mac?

[Patrick Massot]

I know it almost surely won't work because of that *.app thing, but this should be fixable simply by fixing the trylean bash script.

[Alex J. Best]

I downloaded unzipped and ran ./trylean from terminal and got ./trylean: line 4: ./vscodium/codium: No such file or directory

[Alex J. Best]

let me know if i was supposed to do something else!

[Patrick Massot]

Yes, that's expected. The question for MacOS users is: what should I write there?

[Alex J. Best]

There is a folder codium_portable-data

[Patrick Massot]

I know that, from the file explorer, you can click on the folder VSCode.app and it's somehow executed.

[Alex J. Best]

I did some digging but no progress really, it seems that ./vscodium/VSCodium.app/Contents/MacOS/Electron should be the executable file, but it doesn't open in terminal as permission denied, setting chmod u+x on it makes it run with error message

dyld: Library not loaded: @rpath/Electron Framework.framework/Electron Framework
  Referenced from: /Users/alex/Downloads/trylean/./vscodium/VSCodium.app/Contents/MacOS/Electron
  Reason: no suitable image found.  Did find:
    /Users/alex/Downloads/trylean/vscodium/VSCodium.app/Contents/MacOS/../Frameworks/Electron Framework.framework/Electron Framework: file too short
    /Users/alex/Downloads/trylean/vscodium/VSCodium.app/Contents/MacOS/../Frameworks/Electron Framework.framework/Electron Framework: stat() failed with errno=1
Abort trap: 6

I tried to change trylean to that path also but no avail.

Running from finder I get The application can't be opened and after chmod The application is damaged

[Patrick Massot]

Blind shot following https://www.wikihow.com/Open-Applications-Using-Terminal-on-Mac: could you try from the terminal open src -a VSCodium or other variations?

[Alex J. Best]

LSOpenURLsWithRole() failed with error -10810 for the file /Users/alex/Downloads/trylean/vscodium/VSCodium.app.

[Patrick Massot]

Could you try using the full path the the app folder?

[Alex J. Best]

Same result

[Patrick Massot]

This OS is so crazy...

[Patrick Massot]

We'll need to wait for some MacOS expert I'm afraid.

[Patrick Massot]

@Simon Hudon don't you have a Mac somewhere?

[Simon Hudon]

I do have a Mac, I don't know if I qualify as a Mac expert though :P

[Simon Hudon]

I haven't followed this conversation. What is needed?

[Patrick Massot]

Download https://www.imo.universite-paris-saclay.fr/~pmassot/trylean_darwin.zip, unzip. Fix the trylean bash script so that it actually lauches the VSCodium.app sitting next to it (preferably pointing it to the src folder also sitting next to it).

[Patrick Massot]

Note that trylean doesn't have to be a bash script if you know how to turn it into something Mac users could click on (since this seems to be the only supported interaction mode on this OS).

[Simon Hudon]

Bash sounds fine. I'm having a look

[Simon Hudon]

How did you get VSCodium? It doesn't seem to run on my computer

[Patrick Massot]

https://github.com/VSCodium/vscodium/releases/tag/1.42.1

[Patrick Massot]

Maybe I picked the wrong file in this long list

[Patrick Massot]

I guess I picked https://github.com/VSCodium/vscodium/releases/download/1.42.1/VSCodium-darwin-1.42.1.zip

[Patrick Massot]

What happens if you get that zip and try to run its content?

[Simon Hudon]

Then it works

[Simon Hudon]

That's weird

[Simon Hudon]

Here's what I put in the bash file:

#!/bin/bash
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
cd $DIR
open ./vscodium/VSCodium.app $DIR/src

(note the last line)

[Simon Hudon]

Does it come with the Lean plugin? (great bundling by the way)

[Patrick Massot]

Yes, the Lean plugin is there.

[Patrick Massot]

Does this bash script work?

[Patrick Massot]

Or does it work only after you redownload VScodium from the GitHub page?

[Simon Hudon]

Sorry, use this line instead of the last:

open ./vscodium/VSCodium.app --args $DIR/src

[Simon Hudon]

It only works after I redownload VScodium

[Patrick Massot]

This is so weird. This bundle is created by https://gist.github.com/PatrickMassot/567833153f106379b87a20e9d3a712ef

[Simon Hudon]

Opening the directory with VS code doesn't show me any highlighting but I'm asked if I want to install the Lean mode

[Patrick Massot]

If you reinstalled Codium then you probably lost the extension

[Simon Hudon]

I see

[Bryan Gin-ge Chen]

Like Simon, I wasn't able to get the VSCodium app included in trylean_darwin.zip to work. However, it did work after I replaced it with one downloaded from the Github list that you gave. I did, however, run into this issue (mentioned on the VSCodium website):

Note for Mac OS X Mojave users: if you see “App can’t be opened because Apple cannot check it for malicious software” when opening VSCodium the first time, you can right-click the application and choose Open. This should only be required the first time opening on Mojave.

Next I noticed that the extension wasn't detected. I realized that codium_portable-data directory was misnamed. After I renamed it to codium-portable-data, the extension was detected.

When I tried opening the src/ directory, I found I had to fix the permissions of the lean binary to get the extension to run. Then I had to wait a bit for the olean files to recompile. However, the timestamps in the mathlib directory all look OK to me:

$ ls -al
total 9504
drwxr-xr-x@ 67 user  staff    2144 Feb 19 17:33 .
drwxr-xr-x@ 22 user  staff     704 Feb 19 00:13 ..
-rw-r--r--@  1 user  staff   10096 Feb 19 00:13 archimedean.lean
-rw-r--r--@  1 user  staff   81288 Feb 19 00:28 archimedean.olean
-rw-r--r--@  1 user  staff   27278 Feb 19 00:13 associated.lean
-rw-r--r--@  1 user  staff  191932 Feb 19 00:28 associated.olean
-rw-r--r--@  1 user  staff   39866 Feb 19 00:13 big_operators.lean
-rw-r--r--@  1 user  staff  322104 Feb 19 00:31 big_operators.olean
...

[Patrick Massot]

Or maybe it ends up in the wrong location.

[Patrick Massot]

or with the wrong name... sorry about that

[Simon Hudon]

That is a subtle difference. I had to stare at it for a while

[Patrick Massot]

I'd be curious to see whether the mysterious problem disappear if you build the bundle on a Mac. Could you try https://gist.github.com/PatrickMassot/567833153f106379b87a20e9d3a712ef on your computer? (you need python at least 3.6 and the python packages that are used by update-mathlib anyway)

[Patrick Massot]

Note that I updated the gist to fix the typo.

[Patrick Massot]

The hope is one day that script will become part of our CI.

[Bryan Gin-ge Chen]

Hmm, it looks like some timestamps in core lean might be off, possibly due to a timezone issue:

$ ls -al
total 728
drwxrwxr-x@ 17 user  staff     544 Feb 19 17:33 .
drwxrwxr-x@  8 user  staff     256 Feb 19 17:27 ..
-rw-rw-r--@  1 user  staff    6705 Feb 19  2020 bitvec.lean
-rw-rw-r--@  1 user  staff   41762 Feb 19  2020 bitvec.olean
drwxrwxr-x@  4 user  staff     128 Feb 19 17:33 buffer
-rw-rw-r--@  1 user  staff    4607 Feb 19  2020 buffer.lean
-rw-rw-r--@  1 user  staff   33214 Feb 19  2020 buffer.olean
-rw-rw-r--@  1 user  staff    2838 Feb 19  2020 dlist.lean
...

I think the fact that the year is showing up instead of the time indicates that the date is in the future.

Maybe we should add some lines to the script that touch all the lean and olean files just in case.

[Simon Hudon]

Patrick Massot said:

I'd be curious to see whether the mysterious problem disappear if you build the bundle on a Mac. Could you try https://gist.github.com/PatrickMassot/567833153f106379b87a20e9d3a712ef on your computer? (you need python at least 3.6 and the python packages that are used by update-mathlib anyway)

What's the name of the package on pip?

[Patrick Massot]

mathlibtools

[Patrick Massot]

Bryan, do you also see this issue if you get Lean directly from the community release page?

[Patrick Massot]

I mean https://github.com/leanprover-community/lean/releases

[Patrick Massot]

if you get https://github.com/leanprover-community/lean/releases/download/v3.5.1/lean-3.5.1-darwin.zip and unzip, does it have the funny timestamps?

[Patrick Massot]

Probably not, since your funny timestamps are from today

[Rob Lewis]

We really have to get rid of this timestamp checking.

[Patrick Massot]

We still need a way to know when to recompile

[Rob Lewis]

File hashes should be enough to figure that out.

[Patrick Massot]

Isn't it much slower?

[Patrick Massot]

I need to sleep, but I'd be really grateful if Mac users could make progress on this bundle idea. If the MacOS bundle needs to be build from a Mac then I guess we can still ask GitHub actions to do that.

[Rob Lewis]

It's not slower than constantly wondering why mathlib doesn't build, remembering the touch olean script, doing all this crazy debugging.

[Patrick Massot]

Yeah, I really need to sleep, I start seeing non-sense emails (like an email saying "our university got money to fund 25-50 PhD in AI during the next 3 years, could you propose a topic?").

[Patrick Massot]

People are really crazy about AI.

[Bryan Gin-ge Chen]

Bryan, do you also see this issue if you get Lean directly from the community release page?

Just tested it out and I don't see the issue with the downloaded lean. Your mk_bundle.py is still running...

[Bryan Gin-ge Chen]

The VSCodium.app in the output from my run of mk_bundle.py doesn't work either. Maybe the process of downloading and extracting from a script has screwed up the permissions?

[Patrick Massot]

It's worth checking if you can

[Bryan Gin-ge Chen]

I have to run for now but I suspect we're running into some security "feature" of macOS.

[Patrick Massot]

Indeed that sounds very plausible.

[Patrick Massot]

Thank you very much for investigating.

[Sebastien Gouezel]

The security bug has been solved on windows, so I have tried again. Issues:

• trylean.bat should refer to vscodium, not codium
• it tries to recompile everything, so I guess the timestamps are not good (note that I unzipped it respecting the timestamps)

[Patrick Massot]

Do you see bad timestamps?

[Patrick Massot]

Or do you only suspect they exist?

[Sebastien Gouezel]

In fact I don't understand what is going on. The timestamps on the files look good, and if I start lean --make src at the root of the mathlib directory (after having set a suitable path file), it doesn't recompile anything. But still if I launch trylean and open firstproofs.lean the orange bar remains there forever and CPU usage jumps...

[Patrick Massot]

Are you sure the lean --make src that works uses Lean from the bundle and not your regular Lean?

[Sebastien Gouezel]

I am sure it uses my regular Lean, I just wanted to check it if would be happy.

[Patrick Massot]

What happens if you use lean from the bundle?

[Patrick Massot]

it's in lean\bin\lean.exe

[Sebastien Gouezel]

I also tried to open the src directory of trylean with my regular vscode (configured with my regular lean), and the orange bar disappeared right away.

[Sebastien Gouezel]

Indeed, ..\lean\bin\lean.exe --make src tries to recompile everything.

[Patrick Massot]

Can you compare lean --version with ..\lean\bin\lean.exe --version?

[Sebastien Gouezel]

They are the same lean version Lean (version 3.5.1, commit d3a94649bdb4, Release)

[Patrick Massot]

Does the crazy one also try to recompile core lib?

[Patrick Massot]

or only mathlib?

[Sebastien Gouezel]

Only mathlib

[Patrick Massot]

Could you compare timestamps for the (bundled) core lib and mathlib?

[Sebastien Gouezel]

The bundled lean.exe is dated 19/02/2020 18:31, so later than the .lean and .olean files of the library. I don't know if this might matter.

[Patrick Massot]

Can you change that lean.exe time stamp?

[Patrick Massot]

Also, as I wrote above, how do timestamps for the bundled core lib and mathlib compare?

[Sebastien Gouezel]

The bundled core lib timestamps are posterior to mathlib's. I guess this explains the issue.

[Patrick Massot]

Ok, it may be due to the bundles being produced incrementally while I was developing the bundling script. I'll try to regenerate those.

[Patrick Massot]

This is really weird. After running my script, mathlib olean are dated from their actual creation date while core lib get the current timestamp.

[Bryan Gin-ge Chen]

Random guess: maybe the replace in the lines like: next(DIST_LIN.glob('lean-*')).replace(DIST_LIN/'lean') are changing the timestamps?

[Patrick Massot]

Yes, something like this is happening. Instead of guessing I'll try to reset all timestamps before the final zipping

[Patrick Massot]

@Sebastien Gouezel (or other windows users) could you retry from scratch (archive at https://www.imo.universite-paris-saclay.fr/~pmassot/try.html)

[Sebastien Gouezel]

Works perfectly for me.

[Patrick Massot]

Great! Now all the pressure is on MacOS users who still need to debug what happens on their side.

[Bryan Gin-ge Chen]

My suggestion after failing to find any useful info on the gatekeeper is simply to ask macOS users to download VSCodium themselves and put it in the correct directory.

[Patrick Massot]

This is really sad.

[Patrick Massot]

And it wouldn't work because the Lean extension and VScode are intertwined.

[Bryan Gin-ge Chen]

I agree that it's sad. However, it worked for me when I was testing the earlier version of your bundle. You can still include the codium-portable-whatever directory that contains the extension.

[Yufan Lou]

macOS user here, anything need testing?

[Patrick Massot]

The game is to go to https://www.imo.universite-paris-saclay.fr/~pmassot/try.html, download the macos thing, unzip, figure out why MacOS refuses to launch trylean (or VScodium).

[Bryan Gin-ge Chen]

My current theory is that "Gatekeeper" refuses to allow .apps downloaded by scripts on other machines to run.

I just tested the latest version of the bundle, and the following sad workaround steps worked:

• download VSCodium yourself from here (I used the VSCodium-darwin-*.zip link but presumably the .dmg will work as well). Unzip and move VSCodium.app into the vscodium directory, replacing the one that was included.
• change the permission of src/lean/bin/lean to executable
• right-click VSCodium and click "Open" from the menu. A pop-up about not being able to check for malicious whatever will appear, but VSCodium will open.
• drag the src/ directory onto VSCodium (or open directory on src/ from within VSCodium)
• click on first_proofs.lean in VSCodium.

[Yufan Lou]

wow this is the first time that the right-click trick doesn't work on a .app

[Patrick Massot]

Thanks Bryan. This is not much simpler than doing a full install so I guess we'll drop the bundle idea for MacOS.

[Patrick Massot]

For instance there is no longer any technical or legal point in using VScodium instead of VScode with the above procedure (of course there is still the moral argument).

[Patrick Massot]

Bryan, do you understand what is different between the zip file you get from the VScodium release page and the one I created?

[Patrick Massot]

I don't understand how MacOS sees a difference

[Bryan Gin-ge Chen]

No, not really. One thing I noticed is that the executable bits on the lean binaries weren't set after unzipping. Perhaps the same thing happens to the binary files in the .app file and this screws up some hash checking.

[Patrick Massot]

Did you try tweaking the executable bits?

[Bryan Gin-ge Chen]

I did, but I can't be sure that I got them all and I didn't try doing an exhaustive comparison with the downloaded .app.

[Patrick Massot]

Do you have any idea how to do such a comparison?

[Bryan Gin-ge Chen]

Could you look into whether there's a way to fix the executable bits getting changed in the zip / unzip process first? Maybe using .tar.gz instead of ZIP will be more reliable.

[Patrick Massot]

Does MacOS handles tar.gz by default?

[Bryan Gin-ge Chen]

yes

[Patrick Massot]

I won't be able to try now because I'm out of GitHub API quota

[Patrick Massot]

Bryan, (or other Mac users), could you try again using https://www.imo.universite-paris-saclay.fr/~pmassot/trylean_darwin.tar.gz?

[Patrick Massot]

Indeed the zip format is very bad for permissions.

[Alex J. Best]

Ok so opening VScodium.app via double click now works!

[Alex J. Best]

But trylean does not :confused:

[Patrick Massot]

Do you know how to launch VScodium.app from the command line?

[Bryan Gin-ge Chen]

Making VS Code launchable from the command line requires an extra step on macOS; presumably the same thing is true for VScodium.

[Bryan Gin-ge Chen]

(I'll try to test the bundle on my end later today.)

[Alex J. Best]

Lol the problem with trylean was a space in the filename, as I have tested multiple versions of this which extract as trylean 2etc

[Alex J. Best]

Next issue, the lean extension is not picked up.

[Bryan Gin-ge Chen]

I just tested the new bundle, and it didn't open when I double clicked (“VSCodium.app” can’t be opened because Apple cannot check it for malicious software.). I had to right-click VSCodium.app and select "Open" to open it. (I am using macOS 10.14.6 so this is expected, according to the note on https://vscodium.com/). After VSCodium opened, it didn't find the extension. This is apparently related to the quarantine, see the VS Code page on portable mode and macoS. I next removed the quarantine attribute by hand by running xattr -dr com.apple.quarantine VSCodium.app/ and then launched VSCodium. However, the extension still didn't load.

In a final attempt, I tried extracting the bundle again in a new directory, and then I ran the xattr command in the console before opening the app with right click. This time, success! I was able to open VSCodium.app by double clicking, and the extension loaded (and worked perfectly) after I opened the src/ directory.

[Patrick Massot]

Thank you very much Bryan!

[Patrick Massot]

I guess this is almost something we could tell users to do.

[Patrick Massot]

I guess we can't do much more without building a proper installer (which would defeat the purpose of those packages that are guaranteed to install nothing outside of a designated folder and depend on nothing).

[Patrick Massot]

I tried to take up this Lean bundles idea, bringing things up to date. I'd be grateful if people could test things downloaded from https://www.imo.universite-paris-saclay.fr/~pmassot/try.html Remember the idea is that each archive contains an autonomous folder where you can launch trylean and see VScode opening the tutorials project. It probably doesn't work without promising MacOS that you really want to execute this. And maybe you need to unzip the windows file after telling Windows it's safe (or using 7zip).

[Shing Tak Lam]

I just gave the Windows one a shot.

• It took about 5 mins to unzip on my laptop. Which is not bad, but also not great.(Could be due to File Explorer though, CPU usage was below 30%).
• Windows doesn't complain when I unzipped the file, but it does complain when I ran the batch file. If you want to use this with people less familiar with things like this, you need to tell them that the Run button is hidden until the user clicks on "More info"
• mathlib imports work fine, but I get an error with file 'tuto_lib' not found in the LEAN_PATH

[Sebastien Gouezel]

I just tried this on windows. It works perfectly well, even if one extracts the zip file with the in-built windows unzipper (which messes up timestamps -- but timestamps are not relevant with recent versions of Lean, so this is not an issue). The only thing is that, the first time I launched it, there was a security screen saying that this is an unknown program, and that it was not safe to launch it, but if you continue anyway everything is fine.

[Sebastien Gouezel]

Yes, the file tuto_lib is indeed missing from File 5 on.

[Sebastien Gouezel]

Extracting with the standard windows unzipper takes 2 minutes on my desktop, 7-zip takes 10 seconds.

[Patrick Massot]

Thanks! Sorry I forgot about the unusual path setup, I'll fix that. Every line of documentation is welcome. I have no idea how to talk to Windows users and I can't see the issues.

[Kevin Buzzard]

Worked like a dream for me on Ubuntu logged in as me (who already has everything installed of course). I could do everything by clicking (no terminal required) except that when I clicked on the shell script it opened in emacs. Can this file be somehow renamed so that Ubuntu will run it if you click on it?

[Patrick Massot]

Thanks Kevin. All this clicking world is so strange. I'll try to investigate