mystery mathlib errors in `data/list`

Stream: general

[Jean Lo]

I've been trying to get lean+mathlib set up again on my updated work computer now that I'm temporarily un-distracted by exams.

Having brought mathlib up to date, attempting leanpkg build produces complaints beginning with

/usr/home/jlpaca/mathlib/src/data/list/defs.lean:175:4: error: invalid object declaration, environment already has an object named 'list.map_with_index_core._main._meta_aux'
/usr/home/jlpaca/mathlib/src/data/list/defs.lean:181:4: error: invalid definition, a declaration named 'list.map_with_index' has already been declared
/usr/home/jlpaca/mathlib/src/order/lexicographic.lean:31:9: error: infer type failed, unknown variable
  α
/usr/home/jlpaca/mathlib/src/order/lexicographic.lean:69:4: error: rcases tactic failed: a_1 : preorder.le is not an inductive datatype

followed by a bunch more errors in order/lexicographic and eventually a external command exited with status 139. This seems strange to me, since the same code seems to be building happily on CI.

It might be worth mentioning that I'm building lean from source with some changes on FreeBSD. The content of the changes are

• for system-dependent things, do whatever would be done on a linux build, and
• excise some code that depends on procfs. (I previously asked for help about this here. It was/is a temporary fix with the intention that I'd come back and actually implement the BSD version of the functions that report rss.)

but I don't see how any of those things would result in the errors I'm seeing when I attempt to build mathlib, so I'm not entirely sure what's happening.

[Reid Barton]

My guess is that you have some stale .olean files around which are getting loaded

[Jean Lo]

oh, but it happens even when I attempt to build from a fresh clone of leanprover-community/mathlib?

[Reid Barton]

Ohhh, hmm. Is it possible that https://github.com/leanprover/lean/issues/1679 is related?

[Bhavik Mehta]

A fresh clone doesn't update the oleans, I think

[Bhavik Mehta]

Maybe try leanproject get-cache to make sure the oleans are actually updated

[Jalex Stark]

when you say fresh clone, do you mean just doing git clone <url>? what if you make a new clone via leanproject get mathlib?

[Ryan Lahfa]

A way to check for freshness is to just look at the utimes/mtimes of your olean files @Jean Lo

[Ryan Lahfa]

If I recall well, those are used to determine staleness

[Jean Lo]

ah, frick. so I think this is a straightforward case of me being daft.

I checked the definition that lean --make was complaining about, and it turns out that it was added to core after the most recent release of leanprover-community/lean (3.14.0). leanprover-community/mathlib, which just uses 3.14.0, probably doesn't know about that.

...I'll go make everything the correct versions and try this again. It'll probably work.

[Ryan Lahfa]

You got bitten by the algebra/core stuff extraction I guess

[Jean Lo]

right, so with lean 3.14.0 + BSD patches, the thing with data/list/defs goes away.

But apparently something else was causing the errors in order/lexicographic. This still defeats me; the offending line is

instance lex_preorder [preorder α] [preorder β] : preorder (lex α β) :=

about which lean complains it fails to infer the type of the unknown variable α, but also evidently at this point in the code lean recognises α : Type u.

[Kevin Buzzard]

Just use leanproject

[Ryan Lahfa]

Kevin Buzzard said:

Just use leanproject

Does it even work with BSD?
I'm not sure, maybe he needs to patch elan or something :/

[Kevin Buzzard]

Oh I see

[Jean Lo]

(went a fixed another few things that i didn't realise i'd messed up when i edited the lean source. I still don't know what's going on with order/lexicographic, and am going to give up trying to figure it out for now. One day I will probably get an installation of linux or windows for the express purpose of being able to run Lean without having to worry about doing version management by hand.)

[Kevin Buzzard]

Are you compiling mathlib with the version of Lean cited in its leanpkg.toml?

[Jean Lo]

Kevin Buzzard said:

Are you compiling mathlib with the version of Lean cited in its leanpkg.toml?

yes; 3.14.0 with the exception of the BSD patches. So I guess the most reasonable thing to suspect is that I broke something & getting lean to work on BSD isn't as simple as I thought it was. But also whatever I broke would've had to be subtle enough that it didn't affect three-months-ago mathlib, but comes up in the current version.

[Gabriel Ebner]

Please upstream the BSD patches if you want. The map_with_index error is only if you use Lean master, this function got moved from mathlib to Lean after 3.14.0. I have no idea what the lexicographic errors are about.

[Jean Lo]

Gabriel Ebner said:

Please upstream the BSD patches if you want.

I'd love to do that if not for the fact that it ... evidently doesn't work yet :upside_down:

The patches currently live on the freebsd branch of a fork of lean, and all of the present changes have been squashed into a single commit that is not very large (—maybe there's hope that someone will take a look at this and find that it's obvious to them what I've done wrong?)

The map_with_index error is only if you use Lean master, this function got moved from mathlib to Lean after 3.14.0. I have no idea what the lexicographic errors are about.

Yes, I realised my mistake with map_with_index a few hours into this thread. The errors in order/lexicographic persisted even with the correct versions, though, and I haven't since made any progress towards figuring out why they're happening.

[Kevin Buzzard]

Maybe you should post the offending code with the explicit error? It's quite rare around here nowadays that someone posts a problem which nobody can answer, but on the other hand conversations involving BSD are also extremely rare

[Jean Lo]

Yeah, I realise I'm definitely being more trouble than I need to be by, like, not just getting a linux installation up and Just Using Leanproject™, and going there whenever I want to do Lean. But at the same time it'd be nice if this turns out to be something fix-able and I can just have something that works in my usual environment :D

So the errors produced by leanpkg build start with

~/mathlib/src/order/lexicographic.lean:31:9: error: infer type failed, unknown variable
  α
~/mathlib/src/order/lexicographic.lean:69:4: error: rcases tactic failed: a_1 : preorder.le is not an inductive datatype
state:
α : Type u,
β : Type v,
_inst_1 : partial_order α,
_inst_2 : partial_order β,
a₁ : α,
b₁ : β,
a₂ : α,
b₂ : β,
a_1 : (a₁, b₁) ≤ (a₂, b₂),
a_2 : (a₂, b₂) ≤ (a₁, b₁)
⊢ (a₁, b₁) = (a₂, b₂)

more errors follow, but they're mostly just complaints about preorder.lenot being an inductive datatype everywhere it turns up.

The offending code is near the very beginning of order/lexicographic:

instance lex_preorder [preorder α] [preorder β] : preorder (lex α β) :=

at which point lean tells me

infer type failed, unknown variable α

as it does when it tried to compile mathlib. I don't understand why that is, since α was declared a variable a few lines earlier and trying #check α on the line immediately preceding the offending code correctly reports α : Type u.

[Gabriel Ebner]

The patches don't look obviously wrong. Does ctest report any errors?

[Reid Barton]

Hard to imagine what is special about this declaration. Are there any other errors which are not related to lex?

[Reid Barton]

You could try minimizing: replace the proof fields by sorry, inline the data fields, remove the imports, etc

[Reid Barton]

Alternatively, does include α help, as a workaround?

[Kevin Buzzard]

Reid Barton said:

Hard to imagine what is special about this declaration. Are there any other errors which are not related to lex?

Do we have tools nowadays which can list precisely which files in mathlib do not depend on order.lexicographic, and then list which ones of those are leaves in the subgraph? Jean could then try compiling one of these. It would be good to see some more examples of where the BSD version is failing.

[Kevin Buzzard]

Or I guess you could pore through the output of lean --make and try and spot errors which are independent. I don't understand Gabriel's no doubt shrewd comment, but Reid's suggestion of trying to fix the proof might be another way of proceeding. Is BSD Lean passing all the unit tests? Is that what Gabriel just asked?

[Patrick Massot]

leanproject will tell you what depends on a given file, but I haven't made a command telling you what doesn't depend on a file. However you can use the mathlib tools library.

[Gabriel Ebner]

@Kevin Buzzard My question was whether Jean has already run the Lean built-in test suite. Maybe the error occurs there as well and we get a #mwe for free.

[Patrick Massot]

What I mean by "using the library" is going into the mathlib folder, launching ipython and having the following conversation with Python

In [1]: from mathlibtools.lib import LeanProject

In [2]: from pathlib import Path

In [3]: proj = LeanProject.from_path(Path())

In [4]: graph = proj.import_graph

In [5]: [node for node in graph.nodes if node not in graph.descendants('order.lexicographic')]

I can paste the answer if you want but it's pretty long. My point is people shouldn't forget that leanproject is actually a command line wrapper of a library designed to manipulate Lean projects that could do many more specialized things.

[Jean Lo]

oh wow, I have never been so glad to see failed unit tests before:

98% tests passed, 23 tests failed out of 1364

Total Test time (real) = 926.47 sec

The following tests FAILED:
          1 - style_check (Failed)
         12 - lean_print_notation (Failed)
         14 - leantest_all (Failed)
         18 - leantest_123-2.lean (Failed)
         57 - leantest_1952.lean (Failed)
         58 - leantest_1952b.lean (Failed)
         87 - leantest_aux_decl_zeta.lean (Failed)
         93 - leantest_bad_error4.lean (Failed)
        131 - leantest_coe4.lean (Failed)
        132 - leantest_coe5.lean (Failed)
        142 - leantest_cyclic_default_fields.lean (Failed)
        181 - leantest_elab_error_msgs.lean (Failed)
        234 - leantest_inaccessible2.lean (Failed)
        261 - leantest_let1.lean (Failed)
        293 - leantest_non_exhaustive_error.lean (Failed)
        386 - leantest_structure_elab_segfault.lean (Failed)
        449 - leanruntest_all (Failed)
        563 - leanruntest_aexp.lean (Failed)
        775 - leanruntest_ematch_loop.lean (Failed)
        814 - leanruntest_even_odd2.lean (Failed)
        932 - leanruntest_listex2.lean (Failed)
        1005 - leanruntest_nested_inductive_code_gen.lean (Failed)
        1204 - leanruntest_t5.lean (Failed)

[Jean Lo]

(so I guess it's a good time for me to try to go through these & see what the wonky patched version of lean complains about in each case.)

[Jean Lo]

huh, so it seems like the first few of them produce output that agrees with the expected output up until some point where it then complains 'unreachable' code was reached.

[Gabriel Ebner]

Typically, unreachable code should not be reached.

[Jean Lo]

for 123-2, 1952, 1952b, and bad_error4, the unreachable code thing happens when lean is expected to be complaining instead about a type mismatch at field. Other than that it's not clear to me what the errors have in common — e.g. for non_exhaustive_error, unreachable code is reached when

meta def h : name → nat
| `eq := 0

[Mario Carneiro]

Gabriel Ebner said:

Typically, unreachable code should not be reached.

Lean is surprisingly good at reaching the unreachable. I think it is used as a synonym for "off the beaten track"

[Miguel Raz Guzmán Macedo]

Hello @Patrick Massot ! Don't mean to hijack your thread, but would you know of any examples of C++ or Python wrappers of Lean?
I am looking to call Lean from Julia, and a Python or C++ wrapper as an example would help. Thanks!

[Mario Carneiro]

I think @Jason Rute built a python wrapper for ML stuff

[Mario Carneiro]

but I don't think there is an actual FFI interface for lean; it's probably just communicating via IO

[Jason Rute]

(In the future, feel free to start a new thread.)

[Jason Rute]

As for "calling Lean" from another language, this is a vague ask and with many interpretations and many solutions. I'd love to hear more about what you want to do with Lean in Julia. I think we can work out a better answer.

[Jason Rute]

In the mean time, let me tell you a few ways to communicate with Lean.

[Jason Rute]

I moved this discussion to another thread.

[Reid Barton]

@Jean Lo did you ever manage to sort this out? Maybe try https://github.com/leanprover-community/lean/commit/36efb811b4fc435cb8fdf02fad8ba6763e1935fd?

[Reid Barton]

My guess is that this patch doesn't actually work (meaning "produces a working Lean", as opposed to "manages to compile Lean")

[Jean Lo]

very very late reply to @Reid Barton : unfortunately no, I never did manage to get this to work — I eventually decided that trying to figure out the unit tests required an understanding of the internals of lean that I just didn't have. I went and made an attempt to just run the released binary with linux binary compatibility before giving up.

and your guess was right — the patch does make the guards more sensible, but doesn't address any of the things that were causing lean to die in runtime and/or any of the things that were causing the mystery errors in this thread; 3.17.0 compiles on FreeBSD but segfaults as soon as I try to run it.

[Reid Barton]

Doess FreeBSD (or technically the default C ABI or whatever) make any unusual choices regarding the signedness of char, size of int/long, etc? That still seems like the most likely cause to me

[Reid Barton]

Does Lean segfault when building the core library (as part of the build process) or only after that?

[Jean Lo]

I don't trust my memory enough to be entirely sure without running the build again and checking the logs, but iirc it manages to build bin_lean, and then fails when/before building the core library. It was you who pointed out last time that it died because it was trying to readlink from /proc, and I think that's still the case.

[Jean Lo]

re-did the build; confirms the above.

I went and added some of the not-working-yet patches to 3.17.1 just to see what would happen. There've been some changes since the last time I tried; for instance the code in /util/memory.cpp now gives up gracefully when it can't read from /proc/self/statm, where failing to do so used to be fatal. the build still fails the same tests from last time, and I'm still at a loss re: actually trying to fix any of this, but I'm rerunning the failed tests & will be posting the logs/output here once it finishes, on the chance that they turn out to be enlightening to someone else.

[Jean Lo]

LastTest.log

[Bryan Gin-ge Chen]

That's a nearly empty file you just uploaded? The full contents seem to be:

Start testing: Jul 09 02:02 CST
----------------------------------------------------------
End testing: Jul 09 02:02 CST

[Jean Lo]

oh no, you caught that before i could edit the mistake out.

[Jean Lo]

right, that should be the correct file now :innocent:

[Bryan Gin-ge Chen]

FWIW, "Test Failed" appears 22 times, and "Segmentation Fault" appears 5 times. Not bad for 1383 tests, maybe?