Zulip Chat Archive

Stream: general

Topic: mystery mathlib errors in `data/list`


Jean Lo (May 24 2020 at 01:35):

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 (May 24 2020 at 01:38):

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

Jean Lo (May 24 2020 at 01:42):

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

Reid Barton (May 24 2020 at 01:58):

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

Bhavik Mehta (May 24 2020 at 02:12):

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

Bhavik Mehta (May 24 2020 at 02:13):

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

Jalex Stark (May 24 2020 at 02:18):

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 (May 24 2020 at 02:21):

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

Ryan Lahfa (May 24 2020 at 02:21):

If I recall well, those are used to determine staleness

Jean Lo (May 24 2020 at 02:22):

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 (May 24 2020 at 02:24):

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

Jean Lo (May 24 2020 at 02:56):

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 (May 24 2020 at 08:28):

Just use leanproject

Ryan Lahfa (May 24 2020 at 08:41):

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 (May 24 2020 at 08:51):

Oh I see

Jean Lo (May 24 2020 at 18:46):

(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 (May 24 2020 at 19:04):

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

Jean Lo (May 24 2020 at 19:19):

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 (May 25 2020 at 07:41):

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 (May 25 2020 at 16:58):

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 (May 25 2020 at 17:00):

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 (May 25 2020 at 17:16):

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 (May 25 2020 at 17:26):

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

Reid Barton (May 25 2020 at 17:38):

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

Reid Barton (May 25 2020 at 17:39):

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

Reid Barton (May 25 2020 at 17:41):

Alternatively, does include α help, as a workaround?

Kevin Buzzard (May 25 2020 at 17:53):

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 (May 25 2020 at 17:54):

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 (May 25 2020 at 17:58):

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 (May 25 2020 at 18:01):

@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 (May 25 2020 at 18:05):

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 (May 25 2020 at 18:30):

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 (May 25 2020 at 18:32):

(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 (May 25 2020 at 18:45):

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 (May 25 2020 at 18:53):

Typically, unreachable code should not be reached.

Jean Lo (May 25 2020 at 19:07):

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 (May 25 2020 at 19:08):

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 (May 30 2020 at 04:43):

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 (May 30 2020 at 05:07):

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

Mario Carneiro (May 30 2020 at 05:08):

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

Jason Rute (May 30 2020 at 11:43):

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

Jason Rute (May 30 2020 at 11:43):

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 (May 30 2020 at 11:44):

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

Jason Rute (May 30 2020 at 12:44):

I moved this discussion to another thread.

Reid Barton (Jun 03 2020 at 11:51):

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

Reid Barton (Jun 03 2020 at 11:52):

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

Jean Lo (Jul 08 2020 at 13:13):

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 (Jul 08 2020 at 13:20):

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 (Jul 08 2020 at 13:26):

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

Jean Lo (Jul 08 2020 at 23:31):

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 (Jul 09 2020 at 01:25):

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 (Jul 09 2020 at 02:50):

LastTest.log

Bryan Gin-ge Chen (Jul 09 2020 at 02:51):

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 (Jul 09 2020 at 02:52):

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

Jean Lo (Jul 09 2020 at 02:54):

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

Bryan Gin-ge Chen (Jul 09 2020 at 03:00):

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


Last updated: Dec 20 2023 at 11:08 UTC