mathport depending on mathlib

Stream: mathlib4

[Daniel Selsam]

Probably many rough edges still, but it seems to be working. The release at https://github.com/leanprover/mathport/releases/tag/v0.0.0.0 now includes "fake" lake packages for Lean3 and Mathbin. Note: I changed the name from Mathlib to Mathbin to avoid confusion with the existing mathlib4 package. Unless I left a stray reference to my filesystem somewhere by accident, the following should work:

• download the release
• create a new directory TestMathbin with:

1. package.lean

import Lake.Package

open Lake System

def package : Lake.PackageConfig := {
  name := "TestMathbin"
  version := "0.1"
  dependencies := [
    { name := "Mathbin", src := Lake.Source.path (FilePath.mk "<path-to-Lib4>/Mathbin") }
  ]
}

2. TestMathbin.lean with (say) something like:

import Mathlib
import Mathbin

#check Semiring
#lookup3 semiring
#check Semiring_'

example (n : Nat) : n + n = 2 * n := by ring

3. lean-toolchain with leanprover/lean4:nightly-2021-09-24

• lake build should successfully run and print out a few things
• It should also show the LEAN_PATH it used, which can then be used to have the right emacs/vscode setup. For now, I suggest putting export MATHBIN_PATH=<that path> into ~/.bashrc and then e.g. LEAN_PATH=$MATHBIN_PATH emacs . &

The main known rough edge is that we aren't getting errors when Mathport declares new syntax that shadows syntax in Mathlib4. So, some tactics might work when importing Mathlib alone but fail when Mathbin is imported as well. The solution is just to manually remove the syntax declaration from Mathport (e.g. from https://github.com/leanprover/mathport/blob/master/Mathport/Prelude/Syntax.lean#L144).

One other rough edge: due to new name clashes introduced by a weird idiosyncracy of the import graph, I could no longer just add ' at the end of a name to avoid clashes. So, for now I add the more cumbersome _' as in Semiring_' above.

[Daniel Selsam]

Oh and there are many rough edges arises from the old-vs-new structure clashes. For example, there is no instance yet for Semiring_' implying Semiring.

[Daniel Selsam]

(in the process of fixing a few other loose ends...)

[Mac]

@Daniel Selsam You may want to mention which revision of Lake you are using. Especially since you are neither using the latest stable release (i.e. v2.1.0) nor master.

[Daniel Selsam]

Thanks. I see, I hadn't noticed how active lake development has been recently. I am currently using the arbitrary 67470479deaf9f3abe6777c1fb973d7cdbd94182. I will upgrade to v2.1.0 soon (would need to re-run the pipeline to test it).

[Mac]

@Daniel Selsam you are actually using a commit after v2.1.0 (glob support came afterwards), so the only option for upgrading currently is master.

[Scott Morrison]

@Daniel Selsam what is that idiosyncrasy of the import graph? Can we just fix it in mathlib?

[Daniel Selsam]

Scott Morrison said:

Daniel Selsam what is that idiosyncrasy of the import graph? Can we just fix it in mathlib?

If I recall, the issue I hit was related to mul_right_cancel, but there might be more that will only be exposed after fixing that one. I can re-run without the _' change but my guess from grepping is that one of these doesn't import an upstream one:

src/algebra/group/defs.lean:164:lemma mul_right_cancel
src/algebra/group_with_zero/defs.lean:88:lemma mul_right_cancel'
src/algebra/ordered_monoid_lemmas.lean:373:lemma mul_right_cancel''

We can also fix the issue by having a special case in mathport that only uses _' for names in a list.

[Mario Carneiro]

Are you assuming that adding a ' will make it not collide? Mathlib uses names involving ', so you should instead recursively add ' until it is not colliding

[Daniel Selsam]

Mario Carneiro said:

Are you assuming that adding a ' will make it not collide? Mathlib uses names involving ', so you should instead recursively add ' until it is not colliding

I was recursively adding '. The problem is that foo might translate to Foo', but a foo' in mathlib that doesn't import the original foo might translate to Foo' as well. Basically, the recursive '-adding is only relative to the current environment when the declaration is being processed.

[Mario Carneiro]

can we give a local name override?

[Scott Morrison]

Alternatively, can we lint for this in mathlib? Make sure that wherever foo' is declared, foo is already in the environment?

[Mario Carneiro]

I don't think we should demand that in mathlib, but it would be good to collect the list of violators anyway so that mathport can special case them

[Scott Morrison]

It's not like it hurts us overall to do some cleaning up of the foo' messes we have in mathlib. :-)

[Mario Carneiro]

This example seems like a pretty good argument for why that might occur: group and group_with_zero don't directly need each other, but they need to be importable together so one of the names dodges the other

[Daniel Selsam]

Scott Morrison said:

Alternatively, can we lint for this in mathlib? Make sure that wherever foo' is declared, foo is already in the environment?

It might not work if mathlib3 and mathlib4 differ in relevant ways. Recall that I did not hit this issue until mathport started depending on mathlib4. If there is interest I can re-run without _' and figure out exactly what is going wrong.

[Daniel Selsam]

Mario Carneiro said:

can we give a local name override?

Do you mean in mathport? Yes, there is a map in the configuration file for forced renames.

[Mario Carneiro]

How did mathlib4 affect this issue? Why didn't you hit this already in mathlib?

[Daniel Selsam]

Ah, because mathlib3's mul_right_cancel probably clashes with the mathlib4 one, and so became a mul_right_cancel', causing a cascade.

[Daniel Selsam]

I am guessing that before, there were no clashes, and so each of the declarations kept their original names.

[Mario Carneiro]

that sounds like an issue with missing alignments

[Mario Carneiro]

presumably we want mathlib3's mul_right_cancel to become mathlib4's mul_right_cancel

[Daniel Selsam]

aren't the underlying classes implemented differently? we haven't tackled the non-defeq-alignment yet at all.

[Mario Carneiro]

Even if they are, we want them to align

[Mario Carneiro]

we could backport if needed

[Mario Carneiro]

how well can we handle just failing when the non-defeq causes problems, without breaking the build?

[Daniel Selsam]

the build is pretty robust, but everything downstream of a failed decl will fail as well. I could handle theorems differently, so if the decl fails it falls back on trying it as an axiom before giving up.

[Mario Carneiro]

is it possible to use strategic sorry to recover from failed subterms?

[Mario Carneiro]

One possibility is to record that you know a certain alignment is non-defeq, and then whenever that alignment is used you just use sorry instead of creating a known bad term

[Daniel Selsam]

is it possible to use strategic sorry to recover from failed subterms?

It would not be straightforward in the current design, since I am only getting a kernel error (https://github.com/leanprover/mathport/blob/master/Mathport/Binary/Apply.lean#L47) which doesn't return any kind of position information.

[Mario Carneiro]

so the alignment would only be used in e.g. synport

[Mario Carneiro]

Or I suppose you could try to use the alignment at first, and if it fails then fall back to the sorry approach

[Daniel Selsam]

I don't know what the best path is. Nailing non-def-eq alignment will probably be a lot of work (at best), and may not be that relevant if the port goes bottom-up anyway. If we go bottom-up, synport matters much more than binport. We could even refactor so synport only imports mathlib4 oleans instead of binport oleans.

[Scott Morrison]

There's also the argument that having mul_right_cancel and mul_right_cancel' in the first place is confusing as anything. It requires the humans to maintain an internal lookup table of "number of primes" to "mathematical context". I'd be much happier personally with either mul_right_cancel_with_zero or group_with_zero.mul_right_cancel.

[Mario Carneiro]

I'm sympathetic to this but it seems to penalize use of group_with_zero.mul_right_cancel far too much

[Scott Morrison]

So I'd just advocate making whatever changes to mathlib make life easiest for binport+synport.

[Mario Carneiro]

what about mul_right_cancel\0?

[Scott Morrison]

Great!

[Mario Carneiro]

I'm sympathetic to this but it seems to penalize use of group_with_zero.mul_right_cancel far too much

[Mario Carneiro]

what about mul_right_cancel₀?

[Scott Morrison]

I think if the two of you say "this will make life easier for us", that can trump anything else.

[Daniel Selsam]

We could also refactor/extend synport so that every proof is replaced by sorry /- proof in comments -/. Then the port could be two passes:

1. [bottom-up] get the synported files to elaborate in bottom-up order, which will require diagnosing a bunch of not-yet-exhausted elaborator mismatch issues
2. [parallel] removing the sorries in parallel

[Daniel Selsam]

We are working on automation to help with (2), but (1) is essentially unblocked already.

[Mario Carneiro]

One way to achieve (1) is to declare a def' command that ignores its proof argument

[Daniel Selsam]

Nice. theorem_ax?

[Mario Carneiro]

or even does something more interesting, for example: try to elaborate type := proof, fall back on type := sorry, then on sorry := sorry

[Mario Carneiro]

and use info/warn to indicate how successful it was

[Daniel Selsam]

I like the idea that it does its best, but I think it would be disastrous not to have the invariant that all non-proofs were correct. How about only for theorems, and only trying the type := sorry fallback?

[Daniel Selsam]

(and warning if it needed to falllback on sorry, as you suggested)

[Mario Carneiro]

If the type uses tactics or something that doesn't exist we're screwed anyway

[Mario Carneiro]

the point here is to keep going no matter what

[Daniel Selsam]

I was suggesting that (1) be a manual process of touching up the synported files in bottom-up order until they elaborate modulo sorried-proofs.

[Daniel Selsam]

So, when hitting a type with a NYI tactic, somebody would write the tactic at that point before moving on.

[Mario Carneiro]

and individual failures might not be a big problem, depending on how much they are used downstream

[Mario Carneiro]

obviously it's something we would prefer not to deal with but a full stop somewhere in the middle seems like the worst possible response to an error

[Daniel Selsam]

Maybe, but I think it would be a disaster if somebody is trying to do (1) on a file, and struggling for 30m before realizing that the problem is due to some sorry in a definition in a file they have never heard of.

[Daniel Selsam]

How many tactics are used in types/defs? We could also just implement those before we start (1).

[Mario Carneiro]

maybe we can highlight uses of a definition that we know to be broken?

[Mario Carneiro]

we probably won't have to do anything special anyway, if the theorem_ax command reports the errors it encounters during elaboration

[Daniel Selsam]

I am still a little skeptical that we couldn't just implement most/all the necessary tactics for types/defs ahead of time.

[Mario Carneiro]

if you mouse over a definition and it says the type is sorry that should be a pretty strong indicator that something is wrong upstream

[Mario Carneiro]

I am still a little skeptical that we couldn't just implement most/all the necessary tactics for types/defs ahead of time.

I think we can and should, but the best way to find and prioritize those tactics is to have a source file that indicates what needs to be done

[Daniel Selsam]

There are going to be lots of genuine errors that have nothing to do with upstream sorries, e.g. due to failure to synthesize or timeouts in isDefEq. It might take some work to notice that a synthesis call failed because some sorry emerged deep in the trace.

[Mario Carneiro]

I agree that this situation is not great, but it's probably the best we can do after an upstream failure. The situation where those files are just completely broken and you can't even look at them is worse

[Daniel Selsam]

Mario Carneiro said:

I am still a little skeptical that we couldn't just implement most/all the necessary tactics for types/defs ahead of time.

I think we can and should, but the best way to find and prioritize those tactics is to have a source file that indicates what needs to be done

I will defer to you two on how best to find/prioritize these. I assumed (perhaps incorrectly) that there was a short, known list of tactics used in defs/types, or if not known, at least findable on the lean3 side.

[Mario Carneiro]

it should be possible to instrument synport to gather this data

[Daniel Selsam]

Mario Carneiro said:

I agree that this situation is not great, but it's probably the best we can do after an upstream failure. The situation where those files are just completely broken and you can't even look at them is worse

I am fine with having some people plow past sorries in defs/types and keep porting bottom-up, as long as they are adequately informed of the risk that subtle problems might turn out to be caused by upstream sorries.

[Scott Morrison]

Hopefully #9424 will help a bit.

[Johan Commelin]

Thanks!

[Johan Commelin]

Let's wait for CI, and then merge it.

[Scott Morrison]

@Daniel Selsam would you mind documenting somewhere how to run the pipeline? I'd like to get up to speed on this!

I got as far as building lake from source, and cloning https://github.com/leanprover/mathport, but I'm not too sure what to do next. None of the make targets seem to work. I tried running lake build / lake build-lib / lake build-bin in various of the subdirectories that have lakefile.lean files, but without further success.

[Mario Carneiro]

last I checked, lake build-bin in the root directory should work

[Mario Carneiro]

nevermind, I can't build master

[Mario Carneiro]

@Mac I get the following on mathport master / lake master:

$ lake build-bin
./lakefile.lean:1:0: error: could not find native implementation of external declaration 'UInt64.ofNatCore' (symbols 'l_UInt64_ofNatCore___boxed' or 'l_UInt64_ofNatCore')
./lakefile.lean:3:0: error: unknown namespace 'Lake'
./lakefile.lean:11:4: error: expected '→', '->'
error: package configuration (at ./lakefile.lean) has errors

[Scott Morrison]

Sorry, should have been clearer. lake build-bin in the root directory does indeed work for me (to build mathport), but I then don't know how to actually run mathport to process mathlib3.

[Scott Morrison]

(In particular, I don't get the error that you just reported, @Mario Carneiro.)

[Mario Carneiro]

I believe the invocation is something like LEAN_PATH=Lib4 build/bin/Mathport config.json Mathlib::all

[Scott Morrison]

$ LEAN_PATH=Lib4 build/bin/Mathport config.json Mathlib::all
[paths] [{ package := "Mathlib", mod3 := `all }]
[visit] { package := "Mathlib", mod3 := `all }
PANIC at Std.HashMap.find! Std.Data.HashMap:177:14: key is not in the map
uncaught exception: no such file or directory (error code: 2)
  file: /all.tlean

[Mario Carneiro]

You need to get the tleans from the mathport release or build them from mathlib

[Scott Morrison]

How do I build them?

[Mario Carneiro]

I think it's something like lean --make --tlean

[Mario Carneiro]

from the makefile:

    LEAN_PATH=$(LEAN3_LIB):$(MATHLIB3_SRC)  $(LEAN3_BIN)/lean --make --recursive --ast   $(MATHLIB3_SRC)
    LEAN_PATH=$(LEAN3_LIB):$(MATHLIB3_SRC)  $(LEAN3_BIN)/lean --make --recursive --tlean $(MATHLIB3_SRC)
    cp -r $(MATHLIB3_SRC) PreData/Mathlib3

[Scott Morrison]

oh, I see, the makefile isn't meant to work unless you set LEAN3_BIN manually?

[Mario Carneiro]

You don't have to copy mathlib into PreData/Mathlib3 if you modify the config.json file to point at the directory containing .ast.json and .tlean files for mathlib

[Mario Carneiro]

I guess, I don't use the makefile myself since I think Daniel's setup is too specific

[Scott Morrison]

I'm just following it as the only source for knowing how mathport is meant to be used. :-)

[Mario Carneiro]

it looks like LEAN3_BIN, LEAN3_PKG and MATHLIB3_SRC at least need to be set externally

[Mario Carneiro]

I would just set them in the makefile

[Scott Morrison]

It seems strange to even set LEAN3_BIN. Better would just be to change into the right directory and call lean, and let elan pick up the relevant version?

[Mario Carneiro]

I think daniel has this all set up to call master versions of everything

[Scott Morrison]

Is MATHLIB3_SRC intended to be an external copy of mathlib? There's no part of the build script that takes care of pulling mathlib3?

[Mario Carneiro]

yes, it's mathlib master

[Mario Carneiro]

nothing pulls mathlib3 because it's tied to his local copy

[Mario Carneiro]

I think this setup is a bad idea because it's bad for reproducibility, but it's changed a lot recently and I can't quite keep track where it is at

[Scott Morrison]

Ok. Maybe timezones will mesh and I'll be online at the same time as Daniel. :-)

[Scott Morrison]

It would be great if I could clone mathport, read the README, and then run one command to go do a complete run of mathport on the current mathlib3. I was hoping I could update the README file myself to explain this, but it looks like it will take a bit more time.

[Mario Carneiro]

The mathlib steps should work as long as you have any lean/mathlib install

[Mario Carneiro]

that is lean --make --recursive --ast from the src folder in mathlib

[Mario Carneiro]

You might be able to run ast and tlean at the same time, which should be a lot faster

[Mario Carneiro]

lean --make --recursive --ast --tlean

[Scott Morrison]

Ok. I'll try that later, then see if I can get it working all inside mathport.

[Daniel Selsam]

Scott Morrison said:

Daniel Selsam would you mind documenting somewhere how to run the pipeline? I'd like to get up to speed on this!

Yes, and sorry for the headaches you already suffered trying to run it. I had a Dockerfile to do exactly this not so long ago (https://github.com/leanprover/mathport/blob/bfef2071f38728e00a9016e1c547146278469365/docker/Dockerfile) but it went slightly stale so I removed it temporarily. I will revive it this morning.

[Daniel Selsam]

@Scott Morrison I haven't re-run the pipeline in a while, and sadly there is some staleness currently in the Makefile. I will re-run and fix right now.

[Mac]

Mario Carneiro said:

Mac I get the following on mathport master / lake master:

Are you still having trouble? If so, it seems like the issue is that your Lean and Lake versions are probably not aligned with one another. You can verify if this is the case by running lake self-check. If it returns nothing everything is order, if it errors out, then you have problem with version alignment.

[Daniel Selsam]

Daniel Selsam said:

Scott Morrison I haven't re-run the pipeline in a while, and sadly there is some staleness currently in the Makefile. I will re-run and fix right now.

I fixed a bunch of little issues, pushed, re-ran, and posted the lean3 export data, the lean4 output packages, and the logs to https://github.com/leanprover/mathport/releases/tag/v0.0.0.0

For now, in the absence of CI, I would recommend against trying to re-run this yourself and instead just using the releases (and bugging me to re-run whenever there is an important change in one of the many repositories involved).

[Mac]

@Daniel Selsam You may wish to update the commit the v0.0.0.0 tag points to as it currently references one from July 27 which I am sure is not using what is described in the release. :wink:

[Daniel Selsam]

Mac said:

Daniel Selsam You may wish to update the commit the v0.0.0.0 tag points to as it currently references one from July 27 which I am sure is not using what is described in the release. :wink:

Thanks. I have found it (albeit only slightly) convenient to continue updating the same release, so for now I just added the mathport commit to the release description (https://github.com/leanprover/mathport/releases/tag/v0.0.0.0).

[Scott Morrison]

@Daniel Selsam, the new release doesn't seem to include any olean files in the .tar.gz.

[Daniel Selsam]

Do you mean Lean4 oleans or Lean3 oleans? I know they don't contain Lean3 oleans (do you need them?) but I thought they contained the mathported Lean4 oleans.

[Scott Morrison]

No oleans at all.

[Scott Morrison]

Sorry, something is wrong.

[Scott Morrison]

It's just VSCode hiding them from me, sorry. :-(

[Scott Morrison]

I am having another problem, however, that perhaps is real: when I run lake build, I get lots of errors of the form:

failed to write './Lib4/Mathbin/./../leanbin/./lean_packages/mathport/./lean_packages/mathlib/./build/lib/Mathlib/Tactic/NormNum.olean': 2 No such file or directory

[Daniel Selsam]

They are there, but perhaps a little hidden (inside a directory that is usually git-ignored)

[Scott Morrison]

This is perhaps a case sensitivity issue.

[Scott Morrison]

I have ./Lib4/mathbin/, not ./Lib4/Mathbin/.

[Daniel Selsam]

Where are you running lake build? Give me a minute, I will post a .tar.gz of my "TestImport" lake project.

[Scott Morrison]

Ah, great, I was just preparing a git repo with the same purpose. :-)

[Scott Morrison]

In fact, the case sensitivity issues appear to cut both ways: instead of

./Lib4/Mathbin/./../leanbin/./lean_packages/mathport/./lean_packages/mathlib/

I have

./Lib4/mathbin/./../leanbin/./lean_packages/mathport/./lean_packages/Mathlib/
       ^                                                             ^

[Scott Morrison]

I'm running lake build in a directory that contains Lib4, PreData, and Logs, which were creating by unpacking your release file.

[Daniel Selsam]

Here: TestImportMathbin.tar.gz. You should only need to change the path to liquidbin in the lakefile, and then lake build should work and print out something about semirings. If this doesn't work, can you please double-check your lake version against the one in the release description, and also please try downloading the release again (just in case you downloaded in a small window earlier today with a different tar file sitting in the same release)?

[Daniel Selsam]

(I only changed all the package names to be lowercase earlier today, so it is probably just some thing in the pipeline that is a tiny bit stale)

[Daniel Selsam]

Oh also, I am not sure how smart lake is currently regarding stale package dependencies. You might also try removing all lean_packages directories in all the relevant folders.

[Scott Morrison]

Okay, after rebuilding lake at edda065c2fca1495709f9f6c0ad493524b25c574, discarding everything and starting over, running lake build from a directory containing Lib4 and the contents of your TestImportMathbin.tar.gz, I still get error messages like:

failed to write '././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathport/./lean_packages/mathlib/./build/lib/Mathlib/Tactic/Basic.olean': 2 No such file or directory

I'm not sure what's going on. As far as I can see that directory, and indeed that file, exist.

[Scott Morrison]

For hopefully complete reproducibility, my setup is:

git clone https://github.com/leanprover-community/test-mathport
cd test-mathport
make

[Scott Morrison]

I guess that doesn't reproduce compiling lake.

[Daniel Selsam]

@Scott Morrison I have observed a lot of Heisenbug-like issues similar to the one you just posted, that I think are related to lake. Can you just try continuing to type lake build in the TestImportMathbin directory? I just tried from scratch and it took four consecutives builds to work for me.

[Scott Morrison]

Oh dear -- I just checked, and lake is spawning about a dozen separate lean processes. That can't be good. Perhaps these failed to write errors are contentions between different lean processes trying to do the same thing.

[Scott Morrison]

(Would also be consistent with Heisenbugs.)

[Daniel Selsam]

Scott Morrison said:

Oh dear -- I just checked, and lake is spawning about a dozen separate lean processes. That can't be good. Perhaps these failed to write errors are contentions between different lean processes trying to do the same thing.

CC: @Mac

[Daniel Selsam]

@Scott Morrison Were you able to get TestImportMathbin to work eventually? If so, can you please confirm that by copying the LEAN_PATH that lake prints out, you can import from your editor as well?

[Scott Morrison]

Still running lake build repeatedly to see if it stabilises. Some of the stray Lean processes keep running after lake returns to the command line, so I'm waiting for those to end too. Bit of a slow process. :-)

[Scott Morrison]

Oh, exciting variety of errors:

libc++abi.dylib: terminating with uncaught exception of type std::__1::system_error: mutex lock failed: Invalid argument

[Mac]

@Daniel Selsam lake tries to build as many modules as it can in parallel, so spawning many lean processes can be reasonable. While I have encountered some Hisenbugs of my own with lake, I suspect that they are actually lean bugs that emerge when many lean process are trying to load the same .oleans. I have mostly ignored them because, as Hisenbugs, I have no clue how to debug them. The Hisenbugs I have encountered also only seem to appear one Windows (further my suspicion that is due to some race condition with memory mapped oleans).

However, the bugs I have seen are not like yours @Scott Morrison , so I am not quite sure what is going wrong there. Though again, as lake itself is not trying to acquire any locks directly, I would expect either lean has a bug or I am someone violating an invariant of some lean function that I was not aware of.

[Scott Morrison]

(I'm on macos here.)

[Daniel Selsam]

(I'm on linux :))

[Scott Morrison]

@Mac, I don't know anything yet about how lake is working: is it starting a separate lean process for each .lean file that needs to be compiled to an .olean?

[Scott Morrison]

Would you be interested in trying

git clone https://github.com/leanprover-community/test-mathport
cd test-mathport
make

to see if you can reproduce?

[Mario Carneiro]

Scott Morrison said:

Mac, I don't know anything yet about how lake is working: is it starting a separate lean process for each .lean file that needs to be compiled to an .olean?

That's how lean 4 works - it does separate compilation and relies on the build tool to orchestrate the calls

[Scott Morrison]

Great, that's what I thought. I'm just trying to guess how there could be a contention on an .olean file in this setup.

[Scott Morrison]

Note for me this is a pretty reliable heisenbug: lake build is failing every time, albeit with different error messages on different runs.

[Scott Morrison]

I think this might be something to do with it: it seems lake is updating the same dependency multiple times:

mathlib: cloning https://github.com/dselsam/mathlib4.git to ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathlib
mathport: cloning https://github.com/leanprover/mathport.git to ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathport
mathlib: trying to update ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathlib to revision lake
mathport: trying to update ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathport to revision master
mathlib: trying to update ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathlib to revision lake
mathport: trying to update ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathport to revision master
mathlib: trying to update ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathlib to revision lake
mathport: trying to update ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathport to revision master
mathlib: trying to update ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathlib to revision lake
mathport: trying to update ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathport to revision master
mathlib: trying to update ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathport/./lean_packages/mathlib to revision lake
mathlib: trying to update ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathlib to revision lake
mathport: trying to update ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathport to revision master
mathlib: trying to update ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathlib to revision lake
mathport: trying to update ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathport to revision master
mathlib: trying to update ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathport/./lean_packages/mathlib to revision lake
mathlib: trying to update ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathport/./lean_packages/mathlib to revision lake
mathlib: trying to update ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathlib to revision lake

[Scott Morrison]

I've snipped out interspersed output of the form

> LEAN_PATH=././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathlib/./build/lib lean -R ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathlib/./. -o ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathlib/./build/lib/Mathlib/Algebra/Ring/Basic.olean -c ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathlib/./build/ir/Mathlib/Algebra/Ring/Basic.c ././Lib4/liquidbin/./../mathbin/./../leanbin/./lean_packages/mathlib/././Mathlib/Algebra/Ring/Basic.lean

[Scott Morrison]

@Mac, this Dockerfile also reproduces the problem.

FROM ubuntu

USER root

# Set timezone to UTC to avoid prompts from tzdata.
RUN TZ=UTC ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone
# Install prerequisites.
RUN apt-get update && \
    # Lean4 prerequisites:
    apt-get install -y git libgmp-dev cmake ccache gcc-10 g++-10 && \
    apt-get clean
# We need curl to download elan
RUN apt-get install -y curl
# Lake additionally requires some header files for the compiler:
RUN apt-get install -y build-essential

# create a non-root user
RUN useradd -m lean

USER lean
WORKDIR /home/lean

SHELL ["/bin/bash", "-c"]
# set the entrypoint to be a login shell, so everything is on the PATH
ENTRYPOINT ["/bin/bash", "-l"]

# make sure binaries are available even in non-login shells
ENV PATH="/home/lean/.elan/bin:/home/lean/.local/bin:$PATH"

# install elan
RUN curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- -y && \
    . ~/.profile && \
    elan toolchain uninstall stable

RUN git clone https://github.com/leanprover/lake && \
    cd lake && \
    ./build.sh

ENV PATH="/home/lean/lake/build/bin/:$PATH"

# Clone the `test-mathport` repository.
RUN git clone https://github.com/leanprover-community/test-mathport
WORKDIR /home/lean/test-mathport

RUN make download-release
RUN lake build

[Scott Morrison]

(Perhaps it's better to remove the last line, then create a terminal in the generated image and run lake build by hand.)

[Mac]

@Scott Morrison I'll try to take a look at this and debug what I can tomorrow (i.e., in ~10-12 hours).

[Scott Morrison]

Thanks. If there's anything I should try out or investigate, please tell me. I know no one likes a heisenbug. :-(

[Mario Carneiro]

is it possible / does it help to run in single threaded mode?

[Mario Carneiro]

not even sure if lake has an option for that

[Mac]

@Mario Carneiro that is not possible with lake currently

[Scott Morrison]

lake -j 1 says it doesn't know about -j.

[Daniel Selsam]

@Mac FYI here are a few other issues I hit with Lake. I didn't take the time to make repros in case they are easy to fix, but happy to if it would help:

• lake clean throws an error if build directory doesn't exist yet
• I sometimes need to manually link against a lean dependency, despite it being listed as a dependency
• when depending on a cpp project, I need to manually extend CPATH to include the include directory of the relevant lean version
• lake doesn't seem to return an error when builds fail. This one has burned me a bunch of times, because I usually have commands like make && reset && do-thing-that-might-fail-in-20m. And then it fails in 20m for the same reason it failed last time and I don't even see the compiler errors.
• minor/cosmetic: lake build bin silently doesn't build the binary, same with build lib. This causes the same kind of issue as the previous point where I don't know my binary is stale.

[Mac]

Daniel Selsam said:

• lake clean throws an error if build directory doesn't exist yet

@Sebastian Ullrich is that how IO.removeDirAll is intended to work? I was under the impression it was served as a rm -rf not a rm -r (i.e., it be the inverse of IO.createDIrAll). I can of course fix this (by checking the directory exists), but I just wanted to verify that this was the intent for IO.removeDirAll (and if so, that should also probably be included in the comment for the function).

[Sebastian Ullrich]

Sounds like a bug

[Sebastian Ullrich]

Wait no I misunderstood, even the argument path does not exist? I'd expect it to fail then, yes. I'd have to check if the corresponding Rust API, and others, does so as well.

[Sebastian Ullrich]

Technically speaking, the act of removal cannot succeed if the thing to be removed does not exist

[Mac]

@Sebastian Ullrich okay, makes sense, just wanted to verify

[Sebastian Ullrich]

For real fun, see https://github.com/rust-lang/rust/issues/29497

[Mac]

Daniel Selsam said:

• I sometimes need to manually link against a lean dependency, despite it being listed as a dependency
• when depending on a cpp project, I need to manually extend CPATH to include the include directory of the relevant lean version

Could you make issues for these two? I need a mwe for the first one to figure out what is happening there and the later is a feature request that I will need to decide how (and if) I will address it.

[Daniel Selsam]

Mac said:

Daniel Selsam said:

• I sometimes need to manually link against a lean dependency, despite it being listed as a dependency
• when depending on a cpp project, I need to manually extend CPATH to include the include directory of the relevant lean version

Could you make issues for these two? I need a mwe for the first one to figure out what is happening there and the later is a feature request that I will need to decide how (and if) I will address it.

I will try. The second is easy but the first is triggered by a complex project currently.

[Scott Morrison]

I made https://github.com/leanprover/lake/issues/17 to track my problem with running lake build on the mathport artifacts.

[Mac]

Daniel Selsam said:

• lake clean throws an error if build directory doesn't exist yet
• lake doesn't seem to return an error when builds fail. This one has burned me a bunch of times, because I usually have commands like make && reset && do-thing-that-might-fail-in-20m. And then it fails in 20m for the same reason it failed last time and I don't even see the compiler errors.
• minor/cosmetic: lake build bin silently doesn't build the binary, same with build lib. This causes the same kind of issue as the previous point where I don't know my binary is stale.

These 3 are now fixed in master.

[Daniel Selsam]

Mac said:

Daniel Selsam said:

• I sometimes need to manually link against a lean dependency, despite it being listed as a dependency

I need a mwe for the first one to figure out what is happening there

Unfortunately, I can now remove the extra linking argument in my project and it still builds. I have no idea how to reproduce it any more. Maybe it was accidentally fixed in a lake commit between what I am running now and what I was running when I hit the error.