Zulip Chat Archive

Stream: mathlib4

Topic: Mathport oneshot


Mario Carneiro (Oct 24 2022 at 13:16):

I want to bring attention to a new "feature" of mathport (really just some shell script wrangling), oneshot execution, added in mathport#191. You can now write a lean 3 file, add some #aligns in a lean 4 file, and run make oneshot and in less than a second it will do all the work to compile everything and produce a lean 4 output file. This is useful both for mathport developers testing out changes, as well as end users who want to add #aligns and get immediate feedback in the rest of the file.

Kevin Buzzard (Oct 24 2022 at 19:44):

Oh this is super helpful, thanks! I'd been doing all this manually and it was a bit tedious

Scott Morrison (Nov 02 2022 at 22:44):

@Mario Carneiro, do you have an elan override that is making this work? I'm getting

% make oneshot
cd sources/lean && lean --make --recursive --ast --tlean ../../Oneshot/lean3-in
lean: unrecognized option `--make'
Unknown command line option
Lean (version 4.0.0-nightly-2022-10-29, commit 62ec0bfdb02e, Release)

Scott Morrison (Nov 02 2022 at 22:49):

Even if I add an override in sources/lean, I get:

% make oneshot
cd sources/lean && lean --make --recursive --ast --tlean ../../Oneshot/lean3-in
./build/bin/mathport config.oneshot.json Oneshot::main >> Logs/oneshot.out 2> >(tee -a Logs/oneshot.err >&2)
porting Main
uncaught exception: [resolveMod3] failed to resolve 'init'
make: *** [Outputs/src/oneshot/Oneshot/Main.lean] Error 1

Mario Carneiro (Nov 03 2022 at 06:29):

I thought that this override had already been set up by mathport's default installation. make lean3-predata is doing the same thing

Mario Carneiro (Nov 03 2022 at 06:29):

@Scott Morrison

Scott Morrison (Nov 03 2022 at 06:31):

Ah, I see, the makefile target for lean3-predata is creating that elan override, but I guess I have a checked out copy in which I've never run that target.

Mario Carneiro (Nov 03 2022 at 06:31):

oh, lean3-predata does an elan override immediately prior, I'll make the oneshot command do that as well

Moritz Doll (Nov 11 2022 at 07:51):

Lake build fails if I want to run oneshot on a fresh clone of mathport after running make predata (which was successful).

└─$ make oneshot
cd Oneshot/lean3-in && elan override set `cat ../../sources/mathlib/leanpkg.toml | grep lean_version | cut -d '"' -f2`
info: using existing install for 'leanprover-community/lean:3.48.0'
info: override toolchain for '/home/moritz/coding/lean/mathport/Oneshot/lean3-in' set to 'leanprover-community/lean:3.48.0'

  leanprover-community/lean:3.48.0 unchanged - Lean (version 3.48.0, commit 283f6ed8083a, Release)

cd Oneshot/lean3-in && lean --make --recursive --ast --tlean .
cd Oneshot/lean4-in && lake build
error: no such file or directory (error code: 2)
  file: ./../../lean_packages/mathlib/lakefile.lean
make: *** [Makefile:127: Oneshot/lean4-in/build/lib/Oneshot.trace] Error 1

Mario Carneiro (Nov 11 2022 at 13:00):

you also need to build mathport itself (make build or lake build)

Jireh Loreaux (Nov 17 2022 at 22:34):

@Mario Carneiro can you (or someone else who knows how) add some step-by-step instructions for using mathport oneshot to the mathlib4 wiki? I know it was covered in the meeting last week but that audio was really hard to hear in the recording on YouTube, and it would be nice to have them written somewhere anyway.

Rémi Bottinelli (Dec 13 2022 at 06:21):

Hey, i'm getting this error

r@pc-60 ~/P/mathport (master)> make oneshot
cd Oneshot/lean4-in && lake build
warning: manifest out of date: source kind (git/path) of dependency mathlib changed, use `lake update` to update
warning: manifest out of date: source kind (git/path) of dependency std changed, use `lake update` to update
warning: manifest out of date: source kind (git/path) of dependency Qq changed, use `lake update` to update
./build/bin/mathport config.oneshot.json Oneshot::main >> Logs/oneshot.out 2> >(tee -a Logs/oneshot.err >&2)
bash: line 1: Logs/oneshot.out: No such file or directory
make: *** [Makefile:127: Outputs/src/oneshot/Oneshot/Main.lean] Error 1

I've done lake build and make lean3-predata beforehand. Any idea what's wrong?

Reid Barton (Dec 13 2022 at 06:26):

mkdir -p Logs/ first should help

Reid Barton (Dec 13 2022 at 06:27):

It would get created automatically by some of the other targets, but not this one

Rémi Bottinelli (Dec 13 2022 at 06:28):

ah thanks! i did mkdir the Logs at some point but I guess there were other issues at that point, and now that really is the problem/solution.

Rémi Bottinelli (Dec 13 2022 at 06:32):

Mmh, I put this file in main.lean and nothing in the Oneshot.lean part and got:

./build/bin/mathport config.oneshot.json Oneshot::main >> Logs/oneshot.out 2> >(tee -a Logs/oneshot.err >&2)
porting Main
uncaught exception: [resolveMod3] failed to resolve 'combinatorics.quiver.basic'
make: *** [Makefile:127: Outputs/src/oneshot/Oneshot/Main.lean] Error 1

Should I synchronize manually or something?

Mario Carneiro (Dec 13 2022 at 07:28):

you need to get the mathlib release data if you want to import mathlib files

Mario Carneiro (Dec 13 2022 at 07:28):

./download-release.sh nightly-YYYY-MM-DD

Rémi Bottinelli (Dec 13 2022 at 07:29):

Thanks! how do I know which release I want?

Mario Carneiro (Dec 13 2022 at 07:30):

either that or compile them yourself:

./build/bin/mathport --make config.json Mathbin::combinatorics.quiver.basic >> Logs/mathport.out

Mario Carneiro (Dec 13 2022 at 07:30):

I just get yesterday's release

Mario Carneiro (Dec 13 2022 at 07:31):

https://github.com/leanprover-community/mathport/tags

Mario Carneiro (Dec 13 2022 at 07:31):

oh, the syntax might have changed since they are now more than nightly

Rémi Bottinelli (Dec 13 2022 at 07:32):

r@pc-60 ~/P/mathport (master) [2]>

                                   ./download-release.sh nightly-2022-12-12

+ ./download-ported.sh nightly-2022-12-12
+ mkdir -p Outputs/oleans/leanbin/
+ pushd Outputs/oleans/leanbin/
~/Projects/mathport/Outputs/oleans/leanbin ~/Projects/mathport
+ curl -L https://github.com/leanprover-community/mathport/releases/download/nightly-2022-12-12/lean3-binport.tar.gz
+ tar xz
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
100     9  100     9    0     0     45      0 --:--:-- --:--:-- --:--:--    46

gzip: stdin: not in gzip format
tar: Child returned status 1
tar: Error is not recoverable: exiting now

Rémi Bottinelli (Dec 13 2022 at 07:32):

let me see

Mario Carneiro (Dec 13 2022 at 07:32):

you should pick a name that shows up on that list

Mario Carneiro (Dec 13 2022 at 07:33):

(it would be nice if download-release just automatically got the latest version)

Rémi Bottinelli (Dec 13 2022 at 07:33):

I get the same error with predata-nightly-2022-12-13-01

Rémi Bottinelli (Dec 13 2022 at 07:40):

OK, let me recap the process to get Oneshot running:

  1. Clone https://github.com/leanprover-community/mathport/
    git clone https://github.com/leanprover-community/mathport/

  2. get in the folder:
    cd mathport

  3. I had to install cmake and gmp
    sudo dnf install cmake gmp gmp-devel

  4. Run make build

  5. Run make lean3-predata
  6. Get a mathport release with ./download_release $my_choice.
  7. Modify the Oneshot/lean3-in/main.lean file to my wishes.
  8. Run make oneshot

Rémi Bottinelli (Dec 13 2022 at 07:54):

I see the URL for mathlib-predata is

https://github.com/leanprover-community/mathport/releases/download/predata-nightly-2022-12-13-01/mathlib3-predata.tar.gz

while the script tries to get

https://github.com/leanprover-community/mathport/releases/download/predata-nightly-2022-12-13-01/lean3-binport.tar.gz

is that what's going wrong?

Reid Barton (Dec 13 2022 at 08:01):

No these are different things. e.g. the most recent mathport output appears to be https://github.com/leanprover-community/mathport/releases/tag/nightly-2022-12-13-04

Rémi Bottinelli (Dec 13 2022 at 08:03):

Ah, I just chose wrong!

Reid Barton (Dec 13 2022 at 08:03):

For download_release.sh I think you should use one of those version strings e.g. nightly-2022-12-13-04 (one without predata).

Reid Barton (Dec 13 2022 at 08:05):

Don't know why github lists the "releases" in an unhelpful order

Rémi Bottinelli (Dec 13 2022 at 08:05):

how did you find the correct one to use?

Rémi Bottinelli (Dec 13 2022 at 08:06):

because choosing nightly-2022-12-13-01, which I see at the top of the tag page, does not work

Reid Barton (Dec 13 2022 at 08:06):

I used the "Next" button.

Reid Barton (Dec 13 2022 at 08:07):

Are you sure you don't see predata-nightly-2022-12-13-01?

Rémi Bottinelli (Dec 13 2022 at 08:07):

r@pc-60 ~/P/mathport (master)> make oneshot
./build/bin/mathport config.oneshot.json Oneshot::main >> Logs/oneshot.out 2> >(tee -a Logs/oneshot.err >&2)
porting Main
# output is in Outputs/src/oneshot/Oneshot/Main.lean

Rémi Bottinelli (Dec 13 2022 at 08:08):

Reid Barton said:

Are you sure you don't see predata-nightly-2022-12-13-01?

Ah, I do, actually. I thought I just had to strip the predata part!

Reid Barton (Dec 13 2022 at 08:08):

I'm not sure what you need to download specifically for Oneshot to work, but the predata- ones should be used with download-predata.sh and the others with download-release.sh

Mario Carneiro (Dec 13 2022 at 08:08):

You need to download any release which is compatible with the mathlib4 version used to compile mathport

Reid Barton (Dec 13 2022 at 08:10):

Ahh I think github is basing the release "date" on the git commit of mathport itself, so it doesn't realize that newer releases (which are based on more recent versions of mathlib) are better, and should be shown on the first page

Mario Carneiro (Dec 13 2022 at 08:10):

incompatibilities usually manifest as an error saying that the mathport environment could not be loaded because some definition already exists

Mario Carneiro (Dec 13 2022 at 08:11):

I was just about to push a fix to download-release which uses the github API to get the releases and takes the last one, but this is yielding nightly-2022-12-13-01 so it sounds like it is not correct

Reid Barton (Dec 13 2022 at 08:13):

predata-nightly-2022-12-13-01 is the most recent one of those

Heather Macbeth (Dec 13 2022 at 08:17):

@Rémi Bottinelli Just checking, you're not doing this for the mathlib port, are you? If you want to port a mathlib file, the mathport output is already available at
https://github.com/leanprover-community/mathlib3port/tree/master/Mathbin

Rémi Bottinelli (Dec 13 2022 at 08:19):

I want to port a PR that I made and that got in conflict with some port first.
But then, that's good info: If I want to port an existing file (in master), I can just start with your link (?)

Mario Carneiro (Dec 13 2022 at 08:20):

ok it's now getting nightly-2022-12-13-04 via

curl -H "Accept: application/vnd.github+json" -H "X-GitHub-Api-Version: 2022-11-28" \
  https://api.github.com/repos/leanprover-community/mathport/releases \
| jq 'last([.[].tag_name | select(startswith("nightly-"))] | sort | .[])' -r

Rémi Bottinelli (Dec 13 2022 at 08:30):

So I can update my recap with just ./download_release ?

Mario Carneiro (Dec 13 2022 at 08:40):

yes

Eric Wieser (Jan 01 2023 at 12:04):

Can we add some instructions on how to use oneshot on the porting wiki, https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki?

Eric Wieser (Jan 01 2023 at 12:07):

In particular, it would be great if there were a streamlined process for "get the mathport output for a mathlib3 PR"

Patrick Massot (Jan 01 2023 at 12:09):

Note that I tried to improve the documentation of oneshot in https://github.com/leanprover-community/mathport/pull/213 but that PR is somehow stuck because I don't understand Mario's suggestion.

Eric Wieser (Jan 01 2023 at 12:12):

I just pushed a fix that I think addressed Mario's comment; your list was 1, 2, 3, 5, 6, 7, 8 with no 4.

Patrick Massot (Jan 01 2023 at 12:46):

I understood the numbering thing (although I think it would have rendered correctly). But my impression was that Mario also meant something else.

Mario Carneiro (Jan 01 2023 at 21:19):

no, that's what I meant

Reid Barton (Jan 03 2023 at 16:42):

Failure of the day:

mkdir -p Logs/
./build/bin/mathport config.oneshot.json Oneshot::main >> Logs/oneshot.out 2> >(tee -a Logs/oneshot.err >&2)
porting Main
uncaught exception: failed to port Oneshot:Main with imports [Leanbin.Init.Default, Oneshot]:
import Leanbin.Init.Data.Nat.Lemmas failed, environment already contains 'Nat.findX' from Mathlib.Init.Data.Nat.Lemmas
make: *** [Makefile:134: Outputs/src/oneshot/Oneshot/Main.lean] Error 1

Reid Barton (Jan 03 2023 at 16:42):

Any idea about this?

Gabriel Ebner (Jan 03 2023 at 18:34):

My first guess is mismatched Lean/std4/etc. versions. You need to have the same mathport commit (which fixes the dependencies) as the release.

Reid Barton (Jan 05 2023 at 21:46):

omg it worked!

Reid Barton (Jan 05 2023 at 21:46):

It would be nice if it took less than 45 minutes to get a working setup

Reid Barton (Jan 05 2023 at 21:51):

... I wasn't supposed to rm -rf Outputs/, was I.

Heather Macbeth (Jan 08 2023 at 00:56):

Has anyone seen the following oneshot error before? This is my first time trying it.

% make oneshot
cd Oneshot/lean3-in && elan override set `cat ../../sources/mathlib/leanpkg.toml | grep lean_version | cut -d '"' -f2`
cat: ../../sources/mathlib/leanpkg.toml: No such file or directory
error: The following required arguments were not provided:
    <toolchain>

USAGE:
    elan override set <toolchain>

For more information try --help

Mario Carneiro (Jan 08 2023 at 01:03):

That message suggests that sources/mathlib doesn't exist or doesn't have a leanpkg.toml file

Mario Carneiro (Jan 08 2023 at 01:04):

you have to run ./download-release.sh to get a download of mathlib3 first

Eric Wieser (Jan 08 2023 at 01:05):

It would be great if we could setup a gitpod or something that had everything setup in a way that Just Works; but maybe there's too much configuration for that to make sense

Mario Carneiro (Jan 08 2023 at 01:05):

oh, that would be nice

Mario Carneiro (Jan 08 2023 at 01:05):

there is a lot of downloading but not a lot of (mandatory) configuration

Eric Wieser (Jan 08 2023 at 01:06):

I don't know whether that belongs in the gitpod config for mathlib4, or maybe in the mathport repo instead

Mario Carneiro (Jan 08 2023 at 01:07):

I would put it in the mathport repo

Eric Wieser (Jan 08 2023 at 01:07):

It's possible to set up gitpod to open multiple repos in single workspace, if that's at all useful

Mario Carneiro (Jan 08 2023 at 01:07):

@Heather Macbeth Did you follow the directions at https://github.com/leanprover-community/mathport/tree/master/Oneshot ? We may need to make adjustments if the directions don't work

Heather Macbeth (Jan 08 2023 at 01:15):

I did follow the directions. And this is correct:

Mario Carneiro said:

That message suggests that sources/mathlib doesn't exist or doesn't have a leanpkg.toml file

Heather Macbeth (Jan 08 2023 at 01:16):

Earlier I had got this:

% ./download-release.sh
./download-release.sh: line 11: jq: command not found

Heather Macbeth (Jan 08 2023 at 01:17):

But later I tried this and it seemed to work:

% ./download-release.sh nightly-2022-12-13-04
getting release nightly-2022-12-13-04
+ ./download-ported.sh nightly-2022-12-13-04
+ mkdir -p Outputs/oleans/leanbin/
+ pushd Outputs/oleans/leanbin/
[... tons more stuff ...]

Mario Carneiro (Jan 08 2023 at 01:19):

aha, you don't have jq

Mario Carneiro (Jan 08 2023 at 01:20):

are you on a debian such that you can follow the sudo apt ... install instructions?

Heather Macbeth (Jan 08 2023 at 01:20):

mac

Mario Carneiro (Jan 08 2023 at 01:20):

hm, we need something similar for macs

Mario Carneiro (Jan 08 2023 at 01:20):

brew install jq?

Mario Carneiro (Jan 08 2023 at 01:21):

even if you can get the release by specifying it directly, jq is used later in the oneshot script so you will probably want to get it

Heather Macbeth (Jan 08 2023 at 01:24):

OK, ./download_release.sh seems to be doing something now. Thanks!

Heather Macbeth (Jan 28 2023 at 03:08):

Can @Mario Carneiro or someone with experience record how to use oneshot for files with dependencies? Which folder do I put the dependencies in, and what path do I use to refer to them in the import foo line?

Mario Carneiro (Jan 28 2023 at 03:09):

you put the lean 3 files in the lean3-in directory, you can refer to them like top level files

Mario Carneiro (Jan 28 2023 at 03:10):

so lean3-in/foo.lean is referred to in lean3-in/main.lean as import foo

Heather Macbeth (Jan 28 2023 at 03:12):

(delete message about my own mistake, see next message)

Heather Macbeth (Jan 28 2023 at 03:23):

(delete message about my own mistake, see next message)

Heather Macbeth (Jan 28 2023 at 03:26):

Oh :woman_facepalming: My oneshot version of mathlib3 is different from the mathlib3 version of the files I was trying to port, and algebra/order/ring no longer exists.

Heather Macbeth (Jan 28 2023 at 03:32):

After some noise about self-inflicted errors, I do still have problems. Mathport gives me errors like

/Users/heathermacbeth/lean4/mathport/Oneshot/lean3-in/main.lean:1:0: error: file 'arithmetic' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more

where here arithmetic is my foo, located at lean3-in/arithmetic.lean.

Heather Macbeth (Jan 28 2023 at 03:33):

The lean3-in/main.lean file starts

/- Copyright (c) Heather Macbeth, 2022.  All rights reserved. -/

import arithmetic

Heather Macbeth (Jan 28 2023 at 03:38):

Do I need to add lean3-in itself to the path? Currently when I run lean --path from within the lean3-in directory I get the following output:

{
  "is_user_leanpkg_path": false,
  "leanpkg_path_file": "/Users/heathermacbeth/lean4/mathport/Oneshot/lean3-in/leanpkg.path",
  "path": [
    "/Users/heathermacbeth/.elan/toolchains/leanprover-community--lean---3.50.3/bin/../library",
    "/Users/heathermacbeth/.elan/toolchains/leanprover-community--lean---3.50.3/bin/../lib/lean/library",
    "/Users/heathermacbeth/lean4/mathport/Oneshot/lean3-in/../../sources/mathlib/src"
  ]
}

Mario Carneiro (Jan 28 2023 at 03:40):

I think you need to add path . to the leanpkg.path file

Heather Macbeth (Jan 28 2023 at 03:43):

That works! Thank you!

Eric Wieser (Mar 14 2023 at 13:01):

Is there a way to make lake exe cache get work with one-shot?

Eric Wieser (Mar 14 2023 at 13:01):

Right now I seem to have to build the whole thing from scratch, including mathlib4

Mario Carneiro (Mar 17 2023 at 11:01):

AFAIK you should be able to use lake exe cache get in the mathport root, it has a normal dependency on mathlib4 so if you do that and then lake build it should not rebuild mathlib

Eric Wieser (Mar 23 2023 at 19:45):

This doesn't seem to work

Eric Wieser (Mar 23 2023 at 19:45):

At least, it starts building a bunch of Std4 and Aesop (edit: then moves on to mathport)

Eric Wieser (Mar 23 2023 at 19:45):

Repro:

Eric Wieser (Mar 23 2023 at 19:53):

Is it something like mathport using a different version of std4 to what mathlib4 uses?

Eric Wieser (Mar 28 2023 at 22:59):

Gabriel Ebner said:

it seems to rebuild mathlib4 from scratch

Compiling != Building

Gabriel Ebner said:

It will indeed Compile mathlib, but not Build it. This is expected.

resolves my confusion above

Eric Wieser (Mar 28 2023 at 22:59):

My next issue is that make oneshot appears to build ast and tlean files for all the mathlib files consumed by the oneshot/lean-3/main.lean

Eric Wieser (Mar 28 2023 at 23:00):

I did run ./download-release.sh beforehand, as in the readme; did this get a release that didn't match the mathlib3 source?

Kevin Buzzard (Apr 04 2023 at 12:52):

Thought I'd have a go with oneshot again, as I'm porting 8 files manually. Following the instructions here. Step 5 fails for me on Ubuntu 20.04:

~/lean-projects/mathport$ make lean3-source
mkdir -p sources
if [ ! -d "sources/mathlib/.git" ]; then \
    cd sources && git clone https://github.com/leanprover-community/mathlib.git; \
fi
cd sources/mathlib && git clean -xfd && git fetch && git checkout origin/master
Removing leanpkg.path
Removing src/all.lean
HEAD is now at 0ce07501eb chore(linear_algebra/finite_dimensional): generalize from Type to Sort (#18723)
cd sources/mathlib && echo -n 'mathlib commit: ' && git rev-parse HEAD
mathlib commit: 0ce07501ebb0dee26dde9f0805380cf68975dd24
cd sources/mathlib && leanpkg configure && ./scripts/mk_all.sh
configuring mathlib 0.1
mkdir -p sources
if [ ! -d "sources/lean/.git" ]; then \
    cd sources && git clone https://github.com/leanprover-community/lean.git; \
fi
cd sources/lean && git clean -xfd && git checkout `cd ../mathlib && lean --version | sed -e "s/.*commit \([0-9a-f]*\).*/\1/"`
error: pathspec '855e5b74e3a5' did not match any file(s) known to git
make: *** [Makefile:59: lean3-source] Error 1

Any advice? Thanks.

Ruben Van de Velde (Apr 04 2023 at 12:56):

What's in sources/lean?

Eric Wieser (Apr 04 2023 at 12:56):

mathport#231 makes the error clearer

Kevin Buzzard (Apr 04 2023 at 12:59):

Ruben Van de Velde said:

What's in sources/lean?

A copy of lean 3.

$ git status
HEAD detached at 53e8520d8
nothing to commit, working tree clean

Eric Wieser (Apr 04 2023 at 13:01):

It's trying to get https://github.com/leanprover-community/lean/commits/855e5b74e3a5, you seem to have https://github.com/leanprover-community/lean/commits/53e8520d8

Eric Wieser (Apr 04 2023 at 13:01):

I would guess you created this mathport checkout a while ago?

Eric Wieser (Apr 04 2023 at 13:01):

If so, just run git fetch in the sources/lean directory

Kevin Buzzard (Apr 04 2023 at 13:13):

Eric Wieser said:

I would guess you created this mathport checkout a while ago?

I originally cloned it months ago but I ran git pull in the mathport directory an hour or two ago. Did I underpull?

Kevin Buzzard (Apr 04 2023 at 13:13):

Eric Wieser said:

If so, just run git fetch in the sources/lean directory

This fixed it -- thanks!

Ruben Van de Velde (Apr 04 2023 at 13:14):

#232 should fix this issue

Kevin Buzzard (Apr 04 2023 at 13:16):

https://github.com/leanprover-community/mathport/pull/233 for a typo

Floris van Doorn (May 02 2023 at 15:59):

I tried mathport oneshot for the first time today. I managed to get it to work, but maybe the instructions needs some updating:

  • sudo apt install gmp fails on Ubuntu 22.04 (I installed libgmp-dev)
  • I ended up with an empty file config.oneshot.json somehow (maybe because I killed the build process to run lake exe cache get and then restarted the build)
  • Add the instruction to run lake exe cache get
  • Add the instruction to run make lean3-predata (before that I got the error "uncaught exception: [resolveMod3] failed to resolve 'init'") [This was probably me doing something wrong, after removing the whole directory and restarting this was not a problem]

Floris van Doorn (May 02 2023 at 16:45):

Is the ./download-release.sh supposed to download the Lean 3 mathlib cache? If not, that should also be a step added to the instructions. If I don't do it, the oneshot is compiling all of mathlib3 for me. (Doing cd sources/mathlib && leanproject get-cache && cd ../.. seems to fix this - but I got some other trouble that might be caused by this)

Eric Rodriguez (May 23 2023 at 14:09):

oneshot seems to recompile all of mathlib for ast purposes... but I don't see why this is, if everything else is as advertised then oneshot should have the ast for all of mathlib already, and it just needs the new file, no?

Eric Wieser (May 23 2023 at 14:10):

I made this mistake myself; it's re *compile* ing mathlib, but not re-building it.

Eric Rodriguez (May 23 2023 at 14:10):

if it takes as long as it's seeming to take it's still a long time

Eric Rodriguez (May 23 2023 at 15:10):

Yeah, for reference, this gitpod instance doesn't super work - you need to keep doing "something" on it every hour, else it stops due to inactivity

Eric Rodriguez (May 23 2023 at 15:10):

Presumably because it's taking >1hr to do the compilation, which is... a lot for oneshot

Eric Wieser (May 23 2023 at 15:11):

I guess last time I ran it, mathlib4 was half the size...

Mario Carneiro (May 23 2023 at 17:26):

it does not take 1hr to do the compilation. @Scott Morrison and I did this recently and it was closer to 3-5min although I didn't time it

Eric Rodriguez (May 23 2023 at 17:48):

maybe I missed some details because all I did was leave the gitpod window open on one corner

Eric Rodriguez (May 23 2023 at 17:48):

I tried to follow the instructions as verbatim as possible

Mario Carneiro (May 23 2023 at 17:50):

note that the instructions are somewhat incorrect / out of date. Scott and I went through the mathport flow last week and he took some notes that I hope will make it into the docs

Mario Carneiro (May 23 2023 at 17:52):

I mean, if you follow the mathport instructions exactly it will still work, eventually, but there are a few missing commands which cause it to rebuild both mathlib3 and mathlib4 from scratch if you just follow the instructions

Scott Morrison (May 23 2023 at 22:59):

I've written up the instructions and they are now in the README on the projects_instructions branch of mathport. I'm currently getting some people to exercise the instructions for me here!

Brendan Seamas Murphy (Jun 03 2023 at 21:25):

Not sure if anyone has pointed this out, but the build instructions here https://github.com/leanprover-community/mathport/blob/master/Oneshot/README.md don't work using the cl C++ compiler (the visual studio one). Somewhere in the make file the c++ compiler is run with -fPIC, which is supported by clang and g++ but not this one. Might be good to add a caveat about this?

Brendan Seamas Murphy (Jun 03 2023 at 22:36):

I'm trying to run it using clang now but it's defaulting to the wrong target (one where fPIC is not available). Is there a way to get lake build to pass a flag (target) to whatever c compiler it's using to compile FFI.c?

Mario Carneiro (Jun 03 2023 at 22:39):

???

Mario Carneiro (Jun 03 2023 at 22:39):

at no point in the mathport build process should you be dealing with C++ compiler choices

Mario Carneiro (Jun 03 2023 at 22:40):

the makefile only runs lean and lean tools (and grep, sed etc)

Mario Carneiro (Jun 03 2023 at 22:41):

There is no FFI.c file in mathport, I think there might be one in aesop

Mario Carneiro (Jun 03 2023 at 22:42):

but if you are having such problems presumably they also come up when compiling mathlib4

Riccardo Brasca (Jun 04 2023 at 10:02):

I also have a problem with oneshot, at the make lean3-source step: It says

mkdir -p sources
if [ ! -d "sources/mathlib/.git" ]; then \
    cd sources && git clone --depth 1 https://github.com/leanprover-community/mathlib.git; \
fi
cd sources/mathlib && git clean -xfd && git fetch && git checkout "origin/master" --
Removing archive/all.lean
Removing leanpkg.path
Removing src/all.lean
HEAD is now at 5c1efce chore(*): add mathlib4 synchronization comments (#19151)
cd sources/mathlib && echo -n 'mathlib commit: ' && git rev-parse HEAD
mathlib commit: 5c1efce12ba86d4901463f61019832f6a4b1a0d0
cd sources/mathlib && leanpkg configure && ./scripts/mk_all.sh
configuring mathlib 0.1
cd sources/mathlib/archive && git ls-files \
    | sed -n '/\.lean/ { s=\.lean= ; s=/=».«=g; s=^=import «= ; s=»= ; p }' > all.lean
sed: -e expression #1, char 26: unknown option to `s'
make: *** [Makefile:49: mathbin-source] Error 1

Scott Morrison (Jun 04 2023 at 10:16):

@Riccardo Brasca, hmm, that is working for me. Are you possibly running on macos with the standard sed? That is a common problem.

Riccardo Brasca (Jun 04 2023 at 10:16):

I am on Debian

Ruben Van de Velde (Jun 04 2023 at 10:17):

How old is your sed?

Riccardo Brasca (Jun 04 2023 at 10:23):

It is version 4.9

Scott Morrison (Jun 04 2023 at 11:19):

Same for me, interesting.

Eric Wieser (Jun 04 2023 at 11:23):

Could the shell be relevant here? edit: no

Mario Carneiro (Jun 04 2023 at 13:36):

I was also having that bug, it should be fixed on master

Mario Carneiro (Jun 04 2023 at 13:37):

note the line that says s=\.lean= ; - in the makefile it was s=\.lean$== ; but the $= was being treated as a variable reference and it should now be $$= to escape it

Brendan Seamas Murphy (Jun 04 2023 at 22:04):

Okay, I tried switching to use clang on windows subsystem for linux, but I'm still getting an error when it runs lake build. the error is at "[1940/1940] Linking mathport" and comes from calling leanc at some point. Here's the end snippet of the error

error: stderr:
ld.lld: error: ./lake-packages/mathlib/build/ir/Mathlib/Mathport/Rename.o: unknown file type
ld.lld: error: ./lake-packages/mathlib/build/ir/Mathlib/Init/Data/Nat/Notation.o: unknown file type
ld.lld: error: ./lake-packages/std/build/ir/Std/Util/ExtendedBinder.o: unknown file type
ld.lld: error: ./lake-packages/std/build/ir/Std/Classes/SetNotation.o: unknown file type
ld.lld: error: ./lake-packages/std/build/ir/Std/Tactic/OpenPrivate.o: unknown file type
ld.lld: error: ./lake-packages/std/build/ir/Std/Tactic/NoMatch.o: unknown file type
ld.lld: error: ./lake-packages/std/build/ir/Std/Data/Option/Init/Lemmas.o: unknown file type
ld.lld: error: ./lake-packages/std/build/ir/Std/Tactic/HaveI.o: unknown file type
ld.lld: error: ./lake-packages/std/build/ir/Std/Tactic/Unreachable.o: unknown file type
ld.lld: error: ./lake-packages/std/build/ir/Std/Linter/UnreachableTactic.o: unknown file type
ld.lld: error: ./lake-packages/std/build/ir/Std/Lean/TagAttribute.o: unknown file type
ld.lld: error: ./lake-packages/std/build/ir/Std/Lean/AttributeExtra.o: unknown file type
ld.lld: error: ./lake-packages/std/build/ir/Std/Linter/UnnecessarySeqFocus.o: unknown file type
ld.lld: error: ./lake-packages/std/build/ir/Std/Linter.o: unknown file type
ld.lld: error: ./lake-packages/std/build/ir/Std/Util/TermUnsafe.o: unknown file type
ld.lld: error: ./lake-packages/std/build/ir/Std/Tactic/GuardExpr.o: unknown file type
ld.lld: error: ./lake-packages/std/build/ir/Std/Tactic/ByCases.o: unknown file type
ld.lld: error: ./lake-packages/std/build/ir/Std/Tactic/SeqFocus.o: unknown file type
ld.lld: error: ./lake-packages/std/build/ir/Std/Lean/Name.o: unknown file type
ld.lld: error: ./lake-packages/std/build/ir/Std/Lean/Format.o: unknown file type
ld.lld: error: too many errors emitted, stopping now (use --error-limit=0 to see all errors)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `/home/brendan/.elan/toolchains/leanprover--lean4---nightly-2023-05-31/bin/leanc` exited with code 1

Brendan Seamas Murphy (Jun 04 2023 at 23:24):

okay, got it to build! had to install clang within wsl instead of it somehow(?) using the windows level clang (which tried to build for windows). and then I had to use lake clean first before the fix worked

Brendan Seamas Murphy (Jun 04 2023 at 23:28):

possibly the README should just say "don't build on windows"

Mario Carneiro (Jun 05 2023 at 00:16):

the readme is basically "unsupported, you are on your own" for windows, but if you made it work maybe you should contribute some docs since no one else has

Riccardo Brasca (Jun 05 2023 at 07:17):

Mario Carneiro said:

I was also having that bug, it should be fixed on master

Sorry for the late reply. It now works for me, thanks!

Jireh Loreaux (Jun 08 2023 at 16:57):

(deleted) just noise

Jireh Loreaux (Jun 08 2023 at 16:59):

You know what, let me try this from scratch. Maybe I had old artifacts of some sort from when I tried oneshot before. (EDIT: yes, apparently, working from scratch succeeded)

Gabriel Ebner (Jun 08 2023 at 23:26):

Mario Carneiro said:

There is no FFI.c file in mathport, I think there might be one in aesop

Just FYI, there is an FFI.c file in mathport. We use it to access the heartbeat counter in Lean.


Last updated: Dec 20 2023 at 11:08 UTC