Zulip Chat Archive
Stream: lean4
Topic: Explanation of olean files
metakuntyyy (Jun 26 2025 at 13:19):
There is a repository https://github.com/digama0/olean-rs/tree/master that parses .olean files. I'd like to have a upgrade so that it can also parse lean4 .olean files.
What would be the best way, @Mario Carneiro you have written the code, do you know how extensive such a task would be. Are there significant changes compared to lean3 or is this mostly a straightforward endeavour.
metakuntyyy (Jun 26 2025 at 13:38):
Or maybe an alternative question. Can I instead use .ilean files, since they are already human readable? However it seems that the .ilean files do not contain enough information. So I assume that .olean files contain everything, as opposed to .ilean files.
Mario Carneiro (Jun 27 2025 at 15:20):
There is an up to date rust olean parser at https://github.com/digama0/leangz (which is however not set up for just dumping files), and an up to date lean olean parser at https://github.com/digama0/oleandump
metakuntyyy (Jun 27 2025 at 16:42):
Ok, I have tried using the rust parser as I want to use https://github.com/ammkrn/nanoda_lib/ . Currently nanoda_lib uses the lean4export files. I think it would be cool if it also was able to use .olean files.
Everything compiled smoothly, however when copying the leantar binary and the .olean file into a directory and when I execute this
./leantar -k ./Scratch.olean
I get the following
bad .ltar file
Scratch.olean for reference.
import Mathlib
example :2<3:=by norm_num
Here is my lean toolchain, maybe I'm on a too new of a version: leanprover/lean4:v4.21.0-rc3
metakuntyyy (Jun 27 2025 at 16:56):
Oleandump works. I think
Here's my input
prelude
inductive Unity
| unit : Unity
Here's the output:
useGmp = true
leanVersion = 4.21.0-rc3
githash = 6741444a63eec253a7eae7a83f1beb3de015023d
let x198{344} : Array.{0} Lean.Name := array 4 #[`Unity.recOn, `Unity.rec, `Unity.unit, `Unity]
let x218{96} : List.{0} Lean.Name := List.cons #[`u, List.nil]
let x2c0{32} : Lean.Expr := Lean.Expr.const #[`Unity, List.nil]
let x2e0{24} : Lean.Level := Lean.Level.param #[`u]
let x2f8{48} : Lean.Expr := Lean.Expr.sort #[x2e0{24}]
let x310{200} : Lean.Expr := Lean.Expr.forallE #[`t, x2c0{32}, x2f8{48}, Lean.BinderInfo.default]
let x360{24} : Lean.Expr := Lean.Expr.bvar #[1]
let x378{32} : Lean.Expr := Lean.Expr.const #[`Unity.unit, List.nil]
let x398{88} : Lean.Expr := Lean.Expr.app #[x360{24}, x378{32}]
let x3b8{24} : Lean.Expr := Lean.Expr.bvar #[2]
let x3d0{56} : Lean.Expr := Lean.Expr.app #[x3b8{24}, x360{24}]
...
Does this look good?
Mario Carneiro (Jun 28 2025 at 13:53):
metakuntyyy said:
Everything compiled smoothly, however when copying the leantar binary and the .olean file into a directory and when I execute this
./leantar -k ./Scratch.oleanI get the following
bad .ltar file
That's because leantar reads .ltar files not .olean. It compresses .olean files though, if you pass the right arguments
Mario Carneiro (Jun 28 2025 at 13:54):
metakuntyyy said:
Ok, I have tried using the rust parser as I want to use https://github.com/ammkrn/nanoda_lib/ . Currently nanoda_lib uses the lean4export files. I think it would be cool if it also was able to use .olean files.
Probably worth coordinating with @Chris Bailey on this
Mario Carneiro (Jun 28 2025 at 13:55):
metakuntyyy said:
Oleandump works. I think
Does this look good?
Yes that's what it's supposed to look like
metakuntyyy (Jun 28 2025 at 23:13):
Ok thanks for the answers. I have some questions regarding the content and the differences between the lean4export.
In your documentation for the oleandump you mention
Build it with `lake build`, use it like `lake exe oleandump FILE.olean MOD1 MOD2 ...`, where `FILE.olean` is the file to dump and `MOD1 MOD2 ...` are modules that the dump tool itself will load, which will help it resolve references inside the olean file.
something regarding resolving references.
- If I have A.olean and B.olean, and B imports A, and A has a definition that B uses, what do I get when I just dump B without A?
- If I wanted to export the whole mathlib, would I need to take special care, or is it enough to dump all .olean files separately?
- What's the difference contentwise between lean4export and the content of .olean files. Is there something in the content of .olean files that's not in the export or vice versa? (I'm asking this because I had some troubles using lean4export in the past, I don't know if I can export the whole Mathlib, if you have a command that I can plug-and-use I'd be very happy to try it out again.)
For reference, I want to have a project where I can query the lean environment from Rust, as I'm more comfortable writing Rust code than lean code and I want to use the data structures that Rust provides. I'd like to know what I need to do to set up the environment in a way that I get all the information I need.
Mario Carneiro (Jun 29 2025 at 14:07):
The thing about resolving references is really about determining types. It's not required, but it is useful so that you don't just see an object graph of unknown constructors and instead see the names of the constructors. For most of an olean file this information is fixed and built in, e.g. the top level object is a ModuleData and this has Expr in it and oleandump knows about these types without any help. But module data also contains environment extensions, and these are user extensible, so they can have arbitrary types which the dump tool won't know about. If you pass it more modules it can figure these out.
In other words, it will work just fine if you don't pass any modules, but if you declare any custom attributes or other kinds of persistent state then you will get more accurate information if you pass those modules in.
Mario Carneiro (Jun 29 2025 at 14:09):
Note also that environment extensions are superfluous from the perspective of an external lean kernel; they contain only non-logical information.
Mario Carneiro (Jun 29 2025 at 14:14):
metakuntyyy said:
For reference, I want to have a project where I can query the lean environment from Rust, as I'm more comfortable writing Rust code than lean code and I want to use the data structures that Rust provides. I'd like to know what I need to do to set up the environment in a way that I get all the information I need.
Another way to interact with lean from rust is to use https://crates.io/crates/lean-sys and link with lean directly. You can use this to write hybrid programs and call lean APIs from rust.
Mario Carneiro (Jun 29 2025 at 14:16):
(I had a plan for building a safe interface on top of that, but I never finished it. See https://github.com/digama0/lean-rs )
metakuntyyy (Jun 29 2025 at 17:40):
Ok, thanks for the information. I don't plan on working on a typechecker or anything of the sort. I just want to query declarations from rust. From what I've observed is that I like the data structures of nanoda_lib quite well. It seems intuitive and I'd like to query that without any connection from lean besides the export files, either through lean4export or .olean files.
What should I filter from the .olean files. It seems that it has a fixed structure to me, first line is whether gmp is used, second line is the version, third line is the hash. What would be the relevant information, is everything that is a Lean.Expr or a list/array of lean names relevant? Is there anything that I can filter out?
Mario Carneiro (Jun 29 2025 at 17:42):
after that initial header, the whole thing is an in memory data structure written directly to disk, so it has internal pointers to navigate the file
Mario Carneiro (Jun 29 2025 at 17:43):
you can't tell whether something is a Lean.Expr by looking at it, that's what the type information is for
metakuntyyy (Jun 29 2025 at 17:44):
Maybe to give a specific example so that you know what I'd like to do. Given a file like this
import Mathlib
variable (n : ℕ) (p : ℕ) (hp : p ∣ n) {K : Type*} [Field K] [CharP K p]
variable (r : ℕ) (m : K) (hprim : IsPrimitiveRoot m r)
-- Step 1: Define ϕ₁ : ℤ/nℤ → K
def phi1 : ZMod n →+* K :=by
exact ZMod.castHom hp K
-- Step 2: Define ϕ₂ : (ℤ/nℤ)[X] → K via evaluation
def phi2 : Polynomial (ZMod n) →+* K :=
Polynomial.eval₂RingHom (phi1 n p hp) m
-- Step 3: Show X^r - 1 maps to 0, so ϕ₂ descends to the quotient
theorem phi2_vanish (hprim : IsPrimitiveRoot m r) : (phi2 n p hp m)
((Polynomial.X ^ r: Polynomial (ZMod n)) - 1) = (0: K ) :=by
simp [phi2]
rw[IsPrimitiveRoot.pow_eq_one]
simp
exact hprim
I'd like to find all theorems that are used in the proof of phi2_vanish, I know that this is possible to do in lean with metaprogramming, but I'd consider it a success if I can get the same list with my way.
metakuntyyy (Jun 29 2025 at 17:44):
I assume that's possible? And it shouldn't be too hard
Mario Carneiro (Jun 29 2025 at 17:44):
metakuntyyy said:
Ok, thanks for the information. I don't plan on working on a typechecker or anything of the sort. I just want to query declarations from rust. From what I've observed is that I like the data structures of nanoda_lib quite well. It seems intuitive and I'd like to query that without any connection from lean besides the export files, either through lean4export or .olean files.
If you are not wanting to get too in the weeds on this, I highly recommend you just use the Lean APIs for this. Using rust to talk to lean is not easy no matter what you do
metakuntyyy (Jun 29 2025 at 17:45):
Yeah, but I don't want to use rust to talk to lean, I just want to use the data structures in nanoda_lib
Mario Carneiro (Jun 29 2025 at 17:46):
you can do all sorts of useful queries and exploration in a handful of lines in lean. I don't think nanoda_lib is actually designed for general usage, it's a typechecker
Mario Carneiro (Jun 29 2025 at 17:47):
if you want to use the nanoda_lib data structures then you probably should just run nanoda and hook in once it's done, or fork it if you need to modify what it is doing in the middle of typechecking
Mario Carneiro (Jun 29 2025 at 17:47):
and that means just using lean4export files as is
metakuntyyy (Jun 29 2025 at 17:48):
Works for me. Is it currently possible to export the whole Mathlib with lean4export? Do you have a working setup?
metakuntyyy (Jun 29 2025 at 17:48):
Or just specific files that use mathlib?
Mario Carneiro (Jun 29 2025 at 17:49):
I haven't tried it, but I assume you just run lean4export and point to mathlib
metakuntyyy (Jun 29 2025 at 17:57):
This is what I currently get, running in the project relative to lean4export.
lake env ../lean4export/.lake/build/bin/lean4export Mewll3.Primroots
uncaught exception: failed to read file '/home/redacted/Documents/lean/newlean/mewll3/.lake/build/lib/lean/Mewll3/Primroots.olean', invalid header
They run both on an identical version: leanprover/lean4:v4.21.0-rc3
Also see my issue: https://github.com/leanprover/lean4export/issues/5
metakuntyyy (Jun 29 2025 at 17:59):
import Mathlib.Algebra.Order.Ring.Star
import Mathlib.Analysis.Normed.Ring.Lemmas
import Mathlib.Data.Int.Star
import Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- Equivalence of coprime powers of primitive roots. -/
def equiv_primitiveRoots_of_coprimePow {R : Type*} {e r: ℕ} [CommRing R] [IsDomain R][NeZero r](h : e.Coprime r) :
(primitiveRoots r R) ≃ (primitiveRoots r R) := by
have coprmGcdA (x y : ℤ) (hc : IsCoprime x y) : IsCoprime (x.gcdA y) y := by
use x, x.gcdB y
rwa [mul_comm _ y, ← Int.gcd_eq_gcd_ab, Nat.cast_eq_one, ← Int.isCoprime_iff_gcd_eq_one]
have de2 : 0 ≤ (r * Nat.gcdA e r + 1) * Nat.gcdA e r := by
cases le_or_gt 0 (e.gcdA r) with
| inl hc =>
positivity
| inr hc =>
have hr : (0 : ℤ) < r := by exact_mod_cast r.pos_of_neZero
apply Int.mul_nonneg_of_nonpos_of_nonpos _ (Int.le_of_lt hc)
rw [Int.add_le_zero_iff_le_neg', Int.neg_mul_eq_mul_neg]
exact one_le_mul_of_one_le_of_one_le hr (Int.neg_pos_of_neg hc)
have de: 0 ≤(r*(Nat.gcdA e r)+1)*(Nat.gcdA e r) :=by
have cas : 0≤ e.gcdA r ∨ e.gcdA r < 0 :=by exact le_or_gt 0 (e.gcdA r)
have ger : 0 ≤ (r:ℤ):=by exact Int.natCast_nonneg r
cases cas with
| inl hc =>
refine Int.mul_nonneg ?_ hc
refine Int.add_nonneg ?_ ?_
exact Int.mul_nonneg ger hc
positivity
| inr hc =>
rw[right_distrib]
simp only [one_mul, ge_iff_le]
have jj: (r:ℤ)* e.gcdA r *e.gcdA r +e.gcdA r = e.gcdA r *(r*e.gcdA r +1):=by ring
rw[jj]
refine Int.mul_nonneg_iff.mpr ?_
right
constructor
exact Int.le_of_lt hc
have quest : 1 ≤ -(e.gcdA r) :=by exact Int.add_le_zero_iff_le_neg'.mp hc
refine Int.add_le_zero_iff_le_neg'.mpr ?_
rw[neg_mul_eq_mul_neg]
have nez : 1 ≤ (r:ℤ) :=(Int.toNat_le.mp NeZero.one_le)
exact one_le_mul_of_one_le_of_one_le nez quest
have hea (a : R) (ha: a ∈ primitiveRoots r R): a ^ (e * ((r * e.gcdA r + 1) * e.gcdA r).toNat) = a :=by
rw[mem_primitiveRoots] at ha
have fff := IsPrimitiveRoot.val_toRootsOfUnity_coe ha
rw[← fff,← Units.val_pow_eq_pow_val]
congr
rw[← zpow_natCast]
push_cast
have rweq: (↑e * ((↑r * e.gcdA r + 1) * e.gcdA r)) = r*(e* (e.gcdA r)^2)+e*e.gcdA r:=by
ring
rw[Int.natCast_toNat_eq_self.mpr de,rweq,zpow_add,zpow_mul,IsPrimitiveRoot.zpow_eq_one,one_zpow,one_mul]
have hgcd := eq_sub_of_add_eq (Nat.gcd_eq_gcd_ab e r).symm
rw[hgcd,zpow_sub,zpow_mul]
· rw[← Nat.isCoprime_iff_coprime,Int.isCoprime_iff_gcd_eq_one,Int.gcd_natCast_natCast] at h
simp only [h,Nat.cast_one, zpow_one, zpow_natCast]
have last: (((ha.toRootsOfUnity:Rˣ) ^ r) ^ e.gcdB r)⁻¹ = 1 := by
rw[IsPrimitiveRoot.pow_eq_one]
simp only [one_zpow, inv_one]
rwa[← IsPrimitiveRoot.coe_units_iff,fff]
rw[last]
simp only [mul_one]
rwa[← IsPrimitiveRoot.coe_units_iff,fff]
repeat exact Nat.pos_of_neZero r
exact {
toFun μh := ⟨μh.1 ^ e, by
rw[mem_primitiveRoots]
have primr :=μh.2
rw[mem_primitiveRoots] at primr
refine IsPrimitiveRoot.pow_of_coprime primr ?_ ?_
exact h
repeat exact Nat.pos_of_neZero r
⟩
invFun νh := ⟨νh.1 ^ ((r*(Nat.gcdA e r)+1)*(Nat.gcdA e r)).toNat, by
rw[mem_primitiveRoots]
have primr :=νh.2
rw[mem_primitiveRoots] at primr
refine IsPrimitiveRoot.pow_of_coprime primr ?_ ?_
· rw[← Nat.isCoprime_iff_coprime,Int.natCast_toNat_eq_self.mpr de,right_distrib]
simp only [one_mul]
rw[mul_assoc,Int.isCoprime_iff_gcd_eq_one]
simp only [dvd_mul_right, Int.gcd_add_left_left_of_dvd]
rw[← Int.isCoprime_iff_gcd_eq_one]
exact coprmGcdA e r (Nat.Coprime.isCoprime h)
repeat exact Nat.pos_of_neZero r
⟩
left_inv :=by
rw[Function.LeftInverse]
simp only [Subtype.forall, Subtype.mk.injEq]
intro a ha
rw[← pow_mul]
exact hea a ha
right_inv :=by
rw[Function.RightInverse,Function.LeftInverse]
simp only [Subtype.forall, Subtype.mk.injEq]
intro a ha
rw[← pow_mul,mul_comm]
exact hea a ha
}
File in question for reference.
Julian Berman (Jun 29 2025 at 18:00):
It should work, though it will be gigantic, even Init now exports >100MB. I think I used:
lake env lake --dir $DEVELOPMENT/lean4export exe lean4export Mathlib | pv >/dev/null
ran from the Mathlib repo.
(The pv is so I can tell you how big that will be hopefully...)
Julian Berman (Jun 29 2025 at 18:00):
OK looks like:
2.20GiB 0:01:53 [19.9MiB/s] [ <=> ]
Julian Berman (Jun 29 2025 at 18:00):
So.. less huge than I expected.
Mario Carneiro (Jun 29 2025 at 18:02):
metakuntyyy said:
This is what I currently get, running in the project relative to lean4export.
lake env ../lean4export/.lake/build/bin/lean4export Mewll3.Primroots uncaught exception: failed to read file '/home/redacted/Documents/lean/newlean/mewll3/.lake/build/lib/lean/Mewll3/Primroots.olean', invalid headerThey run both on an identical version: leanprover/lean4:v4.21.0-rc3
Also see my issue: https://github.com/leanprover/lean4export/issues/5
That's a version mismatch. There is a back and forth on that issue which apparently got you to build it correctly back then...
Mario Carneiro (Jun 29 2025 at 18:02):
the most likely issue is that the olean file is out of date and you need to lake build first
metakuntyyy (Jun 29 2025 at 18:09):
I don't understand how that can be a version mismatch, the lean4export has leanprover/lean4:v4.21.0-rc3, mewll3 also has leanprover/lean4:v4.21.0-rc3, both versions are equal, both versions have been build with lake build.
Here is the ls of the .olean files
-rw-r--r-- 1 redacted redacted 18353 Jun 29 20:06 Primroots.ilean
-rw-r--r-- 1 redacted redacted 19 Jun 29 20:06 Primroots.ilean.hash
-rw-r--r-- 1 redacted redacted 290912 Jun 29 20:06 Primroots.olean
-rw-r--r-- 1 redacted redacted 19 Jun 29 20:06 Primroots.olean.hash
-rw-r--r-- 1 redacted redacted 3258 Jun 29 20:06 Primroots.trace
built a minute ago. Also last time I didn't try building anything that had mathlib, but maybe I need to do something else? Should I delete the cache and do a fresh build, because I think I have used lake exe cache get to get the mathlib cache.
metakuntyyy (Jun 29 2025 at 18:09):
lake --version
Lake version 5.0.0-6741444 (Lean version 4.21.0-rc3)
Mario Carneiro (Jun 29 2025 at 18:11):
try printing the header of the olean file with xxd | head -10
Mario Carneiro (Jun 29 2025 at 18:11):
it will have the lean version git commit in it
metakuntyyy (Jun 29 2025 at 18:12):
xxd .lake/build/lib/lean/Mewll3/Primroots.olean | head -10
00000000: 6f6c 6561 6e02 0134 2e32 312e 302d 7263 olean..4.21.0-rc
00000010: 3300 0000 0000 0000 0000 0000 0000 0000 3...............
00000020: 0000 0000 0000 0000 3637 3431 3434 3461 ........6741444a
00000030: 3633 6565 6332 3533 6137 6561 6537 6138 63eec253a7eae7a8
00000040: 3366 3162 6562 3364 6530 3135 3032 3364 3f1beb3de015023d
00000050: 0000 bef1 ca32 0000 2870 c2f1 ca32 0000 .....2..(p...2..
00000060: 0000 0000 0100 00f9 0500 0000 0000 0000 ................
00000070: 0500 0000 0000 0000 0400 0000 0000 0000 ................
00000080: 496e 6974 0000 0000 0000 0000 2000 0201 Init........ ...
00000090: 0100 0000 0000 0000 6000 bef1 ca32 0000 ........`....2..
Mario Carneiro (Jun 29 2025 at 18:14):
okay that is the right version
Mario Carneiro (Jun 29 2025 at 18:18):
oh interesting, the error invalid header means it didn't even get to the version check (that's incompatible header)
Chris Bailey (Jun 29 2025 at 18:18):
metakuntyyy said:
Yeah, but I don't want to use rust to talk to lean, I just want to use the data structures in nanoda_lib
Echoing what Mario said, it was intended to be a library with an included binary, but for various reasons its usefulness as a library is questionable. Get in touch with some information about what you intend to do and I'll give you a best guess as to whether it's reasonable to do by importing it as a library.
Mario Carneiro (Jun 29 2025 at 18:19):
this happens when the file either doesn't start with olean or doesn't have sizeof(header) bytes in it and neither of those seems to be the case unless it's having an IO issue reading the file or you pointed at the wrong file
Mario Carneiro (Jun 29 2025 at 18:24):
If I run lake env .lake/build/bin/lean4export Export from lean4export's directory it spews export data, does that work for you?
Chris Bailey (Jun 29 2025 at 18:27):
Just as a sanity check can you dump the header of the Main.olean/Export.olean from your build of lean4export
metakuntyyy (Jun 29 2025 at 18:30):
lake env .lake/build/bin/lean4export Export > /tmp/A.txt
-rw-r--r-- 1 r r 215170656 Jun 29 20:25 A.txt
head /tmp/A.txt
2.0.0
1 #NS 0 Lean
2 #NS 1 Try
3 #NS 2 Config
4 #NS 3 mk
1 #US 0
0 #ES 1
#IND 3 0 0 0 0 0 0 1 3 1 4
5 #NS 0 Bool
6 #NS 5 false
xxd .lake/build/lib/Main.olean | head -10
00000000: 6f6c 6561 6e66 696c 6521 2121 2121 2121 oleanfile!!!!!!!
00000010: 0000 73f5 1e5a 0000 08ea 75f5 1e5a 0000 ..s..Z....u..Z..
00000020: 0000 0000 0100 00f9 0500 0000 0000 0000 ................
00000030: 0500 0000 0000 0000 0400 0000 0000 0000 ................
00000040: 496e 6974 0000 0000 0000 0000 2000 0201 Init........ ...
00000050: 0100 0000 0000 0000 2000 73f5 1e5a 0000 ........ .s..Z..
00000060: 9866 0cb3 c8dc 1e1a 0000 0000 1800 0100 .f..............
00000070: 4800 73f5 1e5a 0000 0000 0000 0000 0000 H.s..Z..........
00000080: 0000 0000 0100 00f9 0700 0000 0000 0000 ................
00000090: 0700 0000 0000 0000 0600 0000 0000 0000 ................
xxd .lake/build/lib/Export.olean | head -10
00000000: 6f6c 6561 6e66 696c 6521 2121 2121 2121 oleanfile!!!!!!!
00000010: 0000 5203 3a59 0000 f8e7 6203 3a59 0000 ..R.:Y....b.:Y..
00000020: 0000 0000 0100 00f9 0500 0000 0000 0000 ................
00000030: 0500 0000 0000 0000 0400 0000 0000 0000 ................
00000040: 496e 6974 0000 0000 0000 0000 2000 0201 Init........ ...
00000050: 0100 0000 0000 0000 2000 5203 3a59 0000 ........ .R.:Y..
00000060: 9866 0cb3 c8dc 1e1a 0000 0000 1800 0100 .f..............
00000070: 4800 5203 3a59 0000 0000 0000 0000 0000 H.R.:Y..........
00000080: 0000 0000 0100 00f9 0500 0000 0000 0000 ................
00000090: 0500 0000 0000 0000 0400 0000 0000 0000 ................
metakuntyyy (Jun 29 2025 at 18:30):
That one works
Mario Carneiro (Jun 29 2025 at 18:32):
oh hey, whats up with those oleanfile!!!!!s
Mario Carneiro (Jun 29 2025 at 18:32):
that's the old header
Mario Carneiro (Jun 29 2025 at 18:33):
I'm not sure exactly how old, I'd guess 8-12 months
Chris Bailey (Jun 29 2025 at 18:33):
#mathlib4 > lake exe cache get errors @ 💬
metakuntyyy (Jun 29 2025 at 18:34):
Yeah, but that one works for some reason. I'm on the up to date branch
git status
On branch master
Your branch is up to date with 'origin/master'.
nothing to commit, working tree clean
metakuntyyy (Jun 29 2025 at 18:34):
Do I delete the .lake directory in lean4export and rebuild again?
Chris Bailey (Jun 29 2025 at 18:35):
Try the lake-manifest.json too.
metakuntyyy (Jun 29 2025 at 18:35):
So, delete both lake-manifest.json and .lake directory, is that correct?
Chris Bailey (Jun 29 2025 at 18:35):
Unless Mario has a better idea.
Mario Carneiro (Jun 29 2025 at 18:35):
If you use lake update it should rebuild the manifest
Mario Carneiro (Jun 29 2025 at 18:36):
although I think you shouldn't need to delete it
metakuntyyy (Jun 29 2025 at 18:36):
Ok, running lake update in lean4export
lake update
info: toolchain not updated; already up-to-date
Mario Carneiro (Jun 29 2025 at 18:36):
(there is nothing in that file anyway)
Mario Carneiro (Jun 29 2025 at 18:37):
so delete the .lake directory and lake build and it should look like it's doing things
metakuntyyy (Jun 29 2025 at 18:43):
Now I get the correct header
xxd .lake/build/lib/lean/Export.olean | head -10
00000000: 6f6c 6561 6e02 0134 2e32 312e 302d 7263 olean..4.21.0-rc
00000010: 3300 0000 0000 0000 0000 0000 0000 0000 3...............
00000020: 0000 0000 0000 0000 3637 3431 3434 3461 ........6741444a
00000030: 3633 6565 6332 3533 6137 6561 6537 6138 63eec253a7eae7a8
00000040: 3366 3162 6562 3364 6530 3135 3032 3364 3f1beb3de015023d
00000050: 0000 5203 3a59 0000 18d8 6803 3a59 0000 ..R.:Y....h.:Y..
00000060: 0000 0000 0100 00f9 0500 0000 0000 0000 ................
00000070: 0500 0000 0000 0000 0400 0000 0000 0000 ................
00000080: 496e 6974 0000 0000 0000 0000 2000 0201 Init........ ...
00000090: 0100 0000 0000 0000 6000 5203 3a59 0000 ........`.R.:Y..
Export still works.
File hashes are identical
sha256sum /tmp/A.txt
46732d7ade2bb2a6cce8ccdac150dbd52050969b2ad509c42c5e51bcef0ebdb1 /tmp/A.txt
sha256sum /tmp/B.txt
46732d7ade2bb2a6cce8ccdac150dbd52050969b2ad509c42c5e51bcef0ebdb1 /tmp/B.txt
The leanexport of my library still doesn't work
lake env ../lean4export/.lake/build/bin/lean4export Mewll3.Primroots > /tmp/Primroots.txt
uncaught exception: failed to read file '/home/redacted/Documents/lean/newlean/mewll3/.lake/build/lib/lean/Mewll3/Primroots.olean', invalid header
metakuntyyy (Jun 29 2025 at 18:44):
Maybe I should delete the lake directory in my library and build from scratch?
Mario Carneiro (Jun 29 2025 at 18:44):
Mario Carneiro said:
If I run
lake env .lake/build/bin/lean4export Exportfrom lean4export's directory it spews export data, does that work for you?
metakuntyyy (Jun 29 2025 at 18:46):
Yeah, that one worked, with both the new and old version.
This is what I ran in the lakeexport directory
lake env .lake/build/bin/lean4export Export > /tmp/B.txt
It produced the file identical to the one before the removal of the .lake directory.
Mario Carneiro (Jun 29 2025 at 18:47):
and does lake env ../lean4export/.lake/build/bin/lean4export Init.Core work too? (from your project directory)
metakuntyyy (Jun 29 2025 at 18:50):
Nope:
lake env ../lean4export/.lake/build/bin/lean4export Init.Core
uncaught exception: failed to read file '/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/lib/lean/Init/Core.olean', invalid header
xxd ~/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/lib/lean/Init/Core.olean | head -10
00000000: 6f6c 6561 6e02 0134 2e32 312e 302d 7072 olean..4.21.0-pr
00000010: 6500 0000 0000 0000 0000 0000 0000 0000 e...............
00000020: 0000 0000 0000 0000 3637 3431 3434 3461 ........6741444a
00000030: 3633 6565 6332 3533 6137 6561 6537 6138 63eec253a7eae7a8
00000040: 3366 3162 6562 3364 6530 3135 3032 3364 3f1beb3de015023d
00000050: 0000 b58f da31 0000 b03b d08f da31 0000 .....1...;...1..
00000060: 0000 0000 0100 00f9 0500 0000 0000 0000 ................
00000070: 0500 0000 0000 0000 0400 0000 0000 0000 ................
00000080: 496e 6974 0000 0000 0000 0000 2000 0201 Init........ ...
00000090: 0100 0000 0000 0000 6000 b58f da31 0000 ........`....1..
Chris Bailey (Jun 29 2025 at 18:54):
I don't really understand Lean's versioning semantics, but pre != rc3.
Chris Bailey (Jun 29 2025 at 18:54):
The CI job github action that runs lean4export on mathlib just uses the cache get result. How did you install mathlib?
Mario Carneiro (Jun 29 2025 at 18:56):
that's also what I get when I look at the same file though
metakuntyyy (Jun 29 2025 at 18:56):
Just using codium and the vscode extension I think. Every time I create a new project.
Mario Carneiro (Jun 29 2025 at 18:57):
what does elan show give?
Mario Carneiro (Jun 29 2025 at 18:57):
in your project
Mario Carneiro (Jun 29 2025 at 18:57):
in particular there might be an 'override', there should not be
metakuntyyy (Jun 29 2025 at 18:59):
In my project
installed toolchains
--------------------
leanprover/lean4:v4.12.0
leanprover/lean4:v4.14.0-rc2
leanprover/lean4:v4.18.0
leanprover/lean4:v4.19.0-rc2
leanprover/lean4:v4.20.1 (resolved from default 'stable')
leanprover/lean4:v4.21.0-rc3
leanprover/lean4:v4.3.0
leanprover/lean4:v4.8.0-rc2
active toolchain
----------------
leanprover/lean4:v4.21.0-rc3 (overridden by '/home/xxx/Documents/lean/newlean/mewll3/lean-toolchain')
Lean (version 4.21.0-rc3, x86_64-unknown-linux-gnu, commit 6741444a63ee, Release)
In my home directory
installed toolchains
--------------------
leanprover/lean4:v4.12.0
leanprover/lean4:v4.14.0-rc2
leanprover/lean4:v4.18.0
leanprover/lean4:v4.19.0-rc2
leanprover/lean4:v4.20.1 (resolved from default 'stable')
leanprover/lean4:v4.21.0-rc3
leanprover/lean4:v4.3.0
leanprover/lean4:v4.8.0-rc2
active toolchain
----------------
leanprover/lean4:v4.20.1 (resolved from default 'stable')
Lean (version 4.20.0, x86_64-unknown-linux-gnu, commit b02228b03f65, Release)
Mario Carneiro (Jun 29 2025 at 19:08):
that all looks correct
Mario Carneiro (Jun 29 2025 at 19:10):
what does lake --version; lake build in your project do?
metakuntyyy (Jun 29 2025 at 19:15):
lake --version; lake build
Lake version 5.0.0-6741444 (Lean version 4.21.0-rc3)
Build completed successfully.
Mario Carneiro (Jun 29 2025 at 19:18):
So lake env ../lean4export/.lake/build/bin/lean4export Init.Core from your project directory fails, while lake env ../lean4export/.lake/build/bin/lean4export Init.Core from lean4export directory works? What do you get if you diff lake env env in those two locations? (There is a lot to redact there so just report what you can spot.)
Mario Carneiro (Jun 29 2025 at 19:22):
maybe a simpler version is lake env bash -c 'echo $LEAN_PATH'
Mario Carneiro (Jun 29 2025 at 19:24):
when I run it I get
lean4export> lake env bash -c 'echo $LEAN_PATH'
/home/mario/Documents/lean/lean4export/.lake/build/lib/lean:/home/mario/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/lib/lean
mathlib4> lake env bash -c 'echo $LEAN_PATH'
/home/mario/Documents/lean/mathlib4/.lake/packages/Cli/.lake/build/lib/lean:/home/mario/Documents/lean/mathlib4/.lake/packages/batteries/.lake/build/lib/lean:/home/mario/Documents/lean/mathlib4/.lake/packages/Qq/.lake/build/lib/lean:/home/mario/Documents/lean/mathlib4/.lake/packages/aesop/.lake/build/lib/lean:/home/mario/Documents/lean/mathlib4/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/mario/Documents/lean/mathlib4/.lake/packages/importGraph/.lake/build/lib/lean:/home/mario/Documents/lean/mathlib4/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/mario/Documents/lean/mathlib4/.lake/packages/plausible/.lake/build/lib/lean:/home/mario/Documents/lean/mathlib4/.lake/build/lib/lean:/home/mario/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/lib/lean
metakuntyyy (Jun 29 2025 at 19:24):
lean4export dir:
CHROME_DESKTOP=code-oss.desktop
COLORTERM=truecolor
DBUS_SESSION_BUS_ADDRESS=unix:path=/run/user/1000/bus
DEBUGINFOD_URLS=https://debuginfod.archlinux.org
DESKTOP_SESSION=plasma
DISPLAY=:1
ELAN_HOME=/home/redacted/.elan
ELAN_TOOLCHAIN=leanprover/lean4:v4.21.0-rc3
GDK_BACKEND=x11
GIT_ASKPASS=/usr/lib/code/extensions/git/dist/askpass.sh
GTK2_RC_FILES=/etc/gtk-2.0/gtkrc:/home/redacted/.gtkrc-2.0:/home/redacted/.config/gtkrc-2.0
GTK_RC_FILES=/etc/gtk/gtkrc:/home/redacted/.gtkrc:/home/redacted/.config/gtkrc
HOME=/home/redacted
ICEAUTHORITY=/run/user/1000/iceauth_LKviYC
INVOCATION_ID=b77258e3c15a4acebd4f47922584eee4
JOURNAL_STREAM=9:25042
KDE_APPLICATIONS_AS_SCOPE=1
KDE_FULL_SESSION=true
KDE_SESSION_UID=1000
KDE_SESSION_VERSION=6
LANG=en_GB.UTF-8
LANGUAGE=
LEAN_RECURSION_COUNT=1
LOGNAME=redacted
MAIL=/var/spool/mail/redacted
MANAGERPID=4155
MEMORY_PRESSURE_WATCH=/sys/fs/cgroup/user.slice/user-1000.slice/user@1000.service/session.slice/plasma-plasmashell.service/memory.pressure
MEMORY_PRESSURE_WRITE=c29tZSAyMDAwMDAgMjAwMDAwMAA=
MOTD_SHOWN=pam
NO_AT_BRIDGE=1
ORIGINAL_XDG_CURRENT_DESKTOP=KDE
PAM_KWALLET5_LOGIN=/run/user/1000/kwallet5.socket
PATH=/home/redacted/Documents/lean/lean4export/.lake/build/bin:/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/bin:/home/redacted/.elan/bin:/home/redacted/bin:/home/redacted/.elan/bin:/usr/local/sbin:/usr/local/bin:/usr/bin:/var/lib/flatpak/exports/bin:/usr/lib/jvm/default/bin:/usr/bin/site_perl:/usr/bin/vendor_perl:/usr/bin/core_perl
PWD=/home/redacted/Documents/lean/lean4export
QT_WAYLAND_RECONNECT=1
SESSION_MANAGER=local/redacted:@/tmp/.ICE-unix/4361,unix/redacted:/tmp/.ICE-unix/4361
SHELL=/bin/bash
SHLVL=1
SYSTEMD_EXEC_PID=4430
TERM=xterm-256color
TERM_PROGRAM=vscode
TERM_PROGRAM_VERSION=1.101.1
USER=redacted
VSCODE_GIT_ASKPASS_EXTRA_ARGS=
VSCODE_GIT_ASKPASS_MAIN=/usr/lib/code/extensions/git/dist/askpass-main.js
VSCODE_GIT_ASKPASS_NODE=/usr/lib/electron35/electron
VSCODE_GIT_IPC_HANDLE=/run/user/1000/vscode-git-cf683f0260.sock
WAYLAND_DISPLAY=wayland-0
XAUTHORITY=/run/user/1000/xauth_fwFXAI
XDG_CONFIG_DIRS=/home/redacted/.config/kdedefaults:/etc/xdg
XDG_CURRENT_DESKTOP=KDE
XDG_DATA_DIRS=/home/redacted/.local/share/flatpak/exports/share:/var/lib/flatpak/exports/share:/usr/local/share:/usr/share
XDG_MENU_PREFIX=plasma-
XDG_RUNTIME_DIR=/run/user/1000
XDG_SEAT=seat0
XDG_SEAT_PATH=/org/freedesktop/DisplayManager/Seat0
XDG_SESSION_CLASS=user
XDG_SESSION_DESKTOP=KDE
XDG_SESSION_ID=5
XDG_SESSION_PATH=/org/freedesktop/DisplayManager/Session3
XDG_SESSION_TYPE=wayland
XDG_VTNR=1
_=/home/redacted/.elan/bin/lake
ELAN=elan
LAKE=/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/bin/lake
LAKE_HOME=/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3
LAKE_PKG_URL_MAP={}
LEAN=/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/bin/lean
LEAN_GITHASH=6741444a63eec253a7eae7a83f1beb3de015023d
LEAN_SYSROOT=/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3
LEAN_AR=/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/bin/llvm-ar
LEAN_PATH=/home/redacted/Documents/lean/lean4export/.lake/build/lib/lean:/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/lib/lean
LEAN_SRC_PATH=/home/redacted/Documents/lean/lean4export:/home/redacted/Documents/lean/lean4export:/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/src/lean/lake
LD_LIBRARY_PATH=/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/lib/lean:/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/lib:/home/redacted/Documents/lean/lean4export/.lake/build/lib
metakuntyyy (Jun 29 2025 at 19:24):
My directory
CHROME_DESKTOP=code-oss.desktop
COLORTERM=truecolor
DBUS_SESSION_BUS_ADDRESS=unix:path=/run/user/1000/bus
DEBUGINFOD_URLS=https://debuginfod.archlinux.org
DESKTOP_SESSION=plasma
DISPLAY=:1
ELAN_HOME=/home/redacted/.elan
ELAN_TOOLCHAIN=leanprover/lean4:v4.21.0-rc3
GDK_BACKEND=x11
GIT_ASKPASS=/usr/lib/code/extensions/git/dist/askpass.sh
GTK2_RC_FILES=/etc/gtk-2.0/gtkrc:/home/redacted/.gtkrc-2.0:/home/redacted/.config/gtkrc-2.0
GTK_RC_FILES=/etc/gtk/gtkrc:/home/redacted/.gtkrc:/home/redacted/.config/gtkrc
HOME=/home/redacted
ICEAUTHORITY=/run/user/1000/iceauth_LKviYC
INVOCATION_ID=b77258e3c15a4acebd4f47922584eee4
JOURNAL_STREAM=9:25042
KDE_APPLICATIONS_AS_SCOPE=1
KDE_FULL_SESSION=true
KDE_SESSION_UID=1000
KDE_SESSION_VERSION=6
LANG=en_GB.UTF-8
LANGUAGE=
LEAN_RECURSION_COUNT=1
LOGNAME=redacted
MAIL=/var/spool/mail/redacted
MANAGERPID=4155
MEMORY_PRESSURE_WATCH=/sys/fs/cgroup/user.slice/user-1000.slice/user@1000.service/session.slice/plasma-plasmashell.service/memory.pressure
MEMORY_PRESSURE_WRITE=c29tZSAyMDAwMDAgMjAwMDAwMAA=
MOTD_SHOWN=pam
NO_AT_BRIDGE=1
ORIGINAL_XDG_CURRENT_DESKTOP=KDE
PAM_KWALLET5_LOGIN=/run/user/1000/kwallet5.socket
PATH=/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/Cli/.lake/build/bin:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/batteries/.lake/build/bin:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/Qq/.lake/build/bin:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/aesop/.lake/build/bin:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/proofwidgets/.lake/build/bin:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/importGraph/.lake/build/bin:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/LeanSearchClient/.lake/build/bin:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/plausible/.lake/build/bin:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/mathlib/.lake/build/bin:/home/redacted/Documents/lean/newlean/mewll3/.lake/build/bin:/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/bin:/home/redacted/.elan/bin:/home/redacted/bin:/home/redacted/.elan/bin:/usr/local/sbin:/usr/local/bin:/usr/bin:/var/lib/flatpak/exports/bin:/usr/lib/jvm/default/bin:/usr/bin/site_perl:/usr/bin/vendor_perl:/usr/bin/core_perl
PWD=/home/redacted/Documents/lean/newlean/mewll3
QT_WAYLAND_RECONNECT=1
SESSION_MANAGER=local/redacted:@/tmp/.ICE-unix/4361,unix/redacted:/tmp/.ICE-unix/4361
SHELL=/bin/bash
SHLVL=1
SYSTEMD_EXEC_PID=4430
TERM=xterm-256color
TERM_PROGRAM=vscode
TERM_PROGRAM_VERSION=1.101.1
USER=redacted
VSCODE_GIT_ASKPASS_EXTRA_ARGS=
VSCODE_GIT_ASKPASS_MAIN=/usr/lib/code/extensions/git/dist/askpass-main.js
VSCODE_GIT_ASKPASS_NODE=/usr/lib/electron35/electron
VSCODE_GIT_IPC_HANDLE=/run/user/1000/vscode-git-76eea6a9f6.sock
WAYLAND_DISPLAY=wayland-0
XAUTHORITY=/run/user/1000/xauth_fwFXAI
XDG_CONFIG_DIRS=/home/redacted/.config/kdedefaults:/etc/xdg
XDG_CURRENT_DESKTOP=KDE
XDG_DATA_DIRS=/home/redacted/.local/share/flatpak/exports/share:/var/lib/flatpak/exports/share:/usr/local/share:/usr/share
XDG_MENU_PREFIX=plasma-
XDG_RUNTIME_DIR=/run/user/1000
XDG_SEAT=seat0
XDG_SEAT_PATH=/org/freedesktop/DisplayManager/Seat0
XDG_SESSION_CLASS=user
XDG_SESSION_DESKTOP=KDE
XDG_SESSION_ID=5
XDG_SESSION_PATH=/org/freedesktop/DisplayManager/Session3
XDG_SESSION_TYPE=wayland
XDG_VTNR=1
_=/home/redacted/.elan/bin/lake
ELAN=elan
LAKE=/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/bin/lake
LAKE_HOME=/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3
LAKE_PKG_URL_MAP={}
LEAN=/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/bin/lean
LEAN_GITHASH=6741444a63eec253a7eae7a83f1beb3de015023d
LEAN_SYSROOT=/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3
LEAN_AR=/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/bin/llvm-ar
LEAN_PATH=/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/Cli/.lake/build/lib/lean:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/batteries/.lake/build/lib/lean:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/Qq/.lake/build/lib/lean:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/aesop/.lake/build/lib/lean:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/importGraph/.lake/build/lib/lean:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/plausible/.lake/build/lib/lean:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/mathlib/.lake/build/lib/lean:/home/redacted/Documents/lean/newlean/mewll3/.lake/build/lib/lean:/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/lib/lean
LEAN_SRC_PATH=/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/Cli:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/batteries:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/batteries:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/Qq:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/aesop:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/aesop:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/proofwidgets:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/proofwidgets:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/importGraph:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/importGraph:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/LeanSearchClient:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/LeanSearchClient:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/plausible:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/plausible:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/mathlib:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/mathlib:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/mathlib:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/mathlib:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/mathlib:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/mathlib:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/mathlib:/home/redacted/Documents/lean/newlean/mewll3:/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/src/lean/lake
LD_LIBRARY_PATH=/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/lib/lean:/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/lib:/home/redacted/Documents/lean/newlean/mewll3/.lake/build/lib:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/mathlib/.lake/build/lib:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/plausible/.lake/build/lib:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/LeanSearchClient/.lake/build/lib:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/importGraph/.lake/build/lib:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/proofwidgets/.lake/build/lib:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/aesop/.lake/build/lib:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/Qq/.lake/build/lib:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/batteries/.lake/build/lib:/home/redacted/Documents/lean/newlean/mewll3/.lake/packages/Cli/.lake/build/lib
metakuntyyy (Jun 29 2025 at 19:25):
This one works in lean4export
lake env ./.lake/build/bin/lean4export Init.Core > /tmp/C.txt
metakuntyyy (Jun 29 2025 at 19:25):
1941510 Jun 29 21:25 C.txt
metakuntyyy (Jun 29 2025 at 19:26):
It fails in my directory
lake env ../lean4export/.lake/build/bin/lean4export Init.Core > /tmp/D.txt
uncaught exception: failed to read file '/home/redacted/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/lib/lean/Init/Core.olean', invalid header
metakuntyyy (Jun 29 2025 at 19:30):
Heh, I have figured out why it failed
metakuntyyy (Jun 29 2025 at 19:30):
I have lean4export installed in both my lean directory and in my newlean directory. I have always used the wrong one.
metakuntyyy (Jun 29 2025 at 19:30):
This one succeeds:
lake env ../../lean4export/.lake/build/bin/lean4export Mewll3.Primroots > /tmp/Primroots.txt
metakuntyyy (Jun 29 2025 at 19:31):
530879985 Jun 29 21:29 Primroots.txt
metakuntyyy (Jun 29 2025 at 19:31):
I'll delete the EVIL directory immediately. :rolling_on_the_floor_laughing:
Mario Carneiro (Jun 29 2025 at 19:34):
Chris Bailey said:
I don't really understand Lean's versioning semantics, but
pre != rc3.
@Sebastian Ullrich I wanted to ask you about this. Why are the distributed olean files reporting a pre-release version, and why is this not causing a version mismatch?
> xxd ~/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/lib/lean/Init/Core.olean | head -10
00000000: 6f6c 6561 6e02 0134 2e32 312e 302d 7072 olean..4.21.0-pr
00000010: 6500 0000 0000 0000 0000 0000 0000 0000 e...............
00000020: 0000 0000 0000 0000 3637 3431 3434 3461 ........6741444a
00000030: 3633 6565 6332 3533 6137 6561 6537 6138 63eec253a7eae7a8
00000040: 3366 3162 6562 3364 6530 3135 3032 3364 3f1beb3de015023d
00000050: 0000 b58f da31 0000 b03b d08f da31 0000 .....1...;...1..
00000060: 0000 0000 0100 00f9 0500 0000 0000 0000 ................
00000070: 0500 0000 0000 0000 0400 0000 0000 0000 ................
00000080: 496e 6974 0000 0000 0000 0000 2000 0201 Init........ ...
00000090: 0100 0000 0000 0000 6000 b58f da31 0000 ........`....1..
> xxd .lake/build/lib/lean/Mathlib.olean | head -10
00000000: 6f6c 6561 6e02 0134 2e32 312e 302d 7263 olean..4.21.0-rc
00000010: 3300 0000 0000 0000 0000 0000 0000 0000 3...............
00000020: 0000 0000 0000 0000 3637 3431 3434 3461 ........6741444a
00000030: 3633 6565 6332 3533 6137 6561 6537 6138 63eec253a7eae7a8
00000040: 3366 3162 6562 3364 6530 3135 3032 3364 3f1beb3de015023d
00000050: 0000 a102 490f 0000 40c2 aa02 490f 0000 ....I...@...I...
00000060: 0000 0000 0100 00f9 0500 0000 0000 0000 ................
00000070: 0500 0000 0000 0000 0400 0000 0000 0000 ................
00000080: 496e 6974 0000 0000 0000 0000 2000 0201 Init........ ...
00000090: 0100 0000 0000 0000 6000 a102 490f 0000 ........`...I...
metakuntyyy (Jun 29 2025 at 19:35):
find . | grep Export.lean
./newfolder/lean4export/Export.lean
./lean4export/Export.lean
Yes my project is in newfolder, yes, I've updated the lean4export in the root directory. no I don't have an idea why I've cloned the repository twice.
Well sorry for wasting your time for my stupidity. But at least I can now try to fiddle with nanoda.
metakuntyyy (Jun 29 2025 at 19:36):
Good riddance.
newfolder]$ rm -r lean4export/
metakuntyyy (Jun 29 2025 at 19:41):
Chris Bailey said:
metakuntyyy said:
Yeah, but I don't want to use rust to talk to lean, I just want to use the data structures in nanoda_lib
Echoing what Mario said, it was intended to be a library with an included binary, but for various reasons its usefulness as a library is questionable. Get in touch with some information about what you intend to do and I'll give you a best guess as to whether it's reasonable to do by importing it as a library.
Now that I have exported my project and received a 500MB dump, all I want to do is find the declaration in my .lean file
import Mathlib.Algebra.Order.Ring.Star
import Mathlib.Analysis.Normed.Ring.Lemmas
import Mathlib.Data.Int.Star
import Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- Equivalence of coprime powers of primitive roots. -/
def equiv_primitiveRoots_of_coprimePow {R : Type*} {e r: ℕ} [CommRing R] [IsDomain R][NeZero r](h : e.Coprime r) :
If I manage to find equiv_primitiveRoots_of_coprimePow in the dump I am happy for now. After that I'll tinker a little bit and see what's possible with nanoda.
metakuntyyy (Jun 29 2025 at 19:42):
I know it's in the dump
cat /tmp/Primroots.txt | grep equiv_primitiveRoots_of_coprimePow
724031 #NS 0 equiv_primitiveRoots_of_coprimePow
So I'm excited to play with it a bit.
Mario Carneiro (Jun 29 2025 at 19:48):
that's actually just the declaration of the name. You should be able to find the definition if you look for a #DEF 724031
Mario Carneiro (Jun 29 2025 at 19:49):
in fact, I wouldn't be surprised if it's the last line in the file
metakuntyyy (Jun 29 2025 at 19:52):
It works, I get this on a grep
cat Primroots.txt | grep ' 724031 '
724032 #NS 724031 _proof_4
724039 #NS 724031 _proof_5
724053 #NS 724031 _proof_1
724054 #NS 724031 _proof_6
724063 #NS 724031 _proof_7
724068 #NS 724031 _proof_8
724071 #NS 724031 _proof_2
724072 #NS 724031 _proof_9
724075 #NS 724031 _proof_3
724076 #NS 724031 _proof_10
724077 #NS 724031 _proof_11
#DEF 724031 15844705 15844824 R 31 41
This is the tail:
tail Primroots.txt
17559576 #EA 17559575 2
17559577 #EA 17559573 17559576
17559578 #EA 17559577 2
17559579 #EP #BC 699992 17300154 17559578
17559580 #EP #BI 24 97 17559579
17559581 #EA 2900 17300155
17559582 #EA 17559581 17559576
17559583 #EL #BC 12 17300154 17559582
17559584 #EL #BI 24 97 17559583
#THM 806245 17559580 17559584 41
I have no idea what the _proof_* objects are supposed to mean. I think they are hidden constants added by the tactics to prove my theorem.
Mario Carneiro (Jun 29 2025 at 19:53):
#NS are just name declarations
Mario Carneiro (Jun 29 2025 at 19:53):
try using #print equiv_primitiveRoots_of_coprimePow and you will probably see those proof_n things
Mario Carneiro (Jun 29 2025 at 19:54):
they are abstracted proof parts of a definition
Mario Carneiro (Jun 29 2025 at 19:55):
the last thing proved is a theorem, probably the definitional equation for your definition
metakuntyyy (Jun 29 2025 at 19:55):
How do I set the threshold again. set_option pp.threshold 0?
Mario Carneiro (Jun 29 2025 at 19:55):
threshold of what
metakuntyyy (Jun 29 2025 at 19:55):
To pretty print the proof
metakuntyyy (Jun 29 2025 at 19:56):
It is hidden :
def equiv_primitiveRoots_of_coprimePow.{u_1} : {R : Type u_1} →
{e r : ℕ} →
[inst : CommRing R] →
[inst_1 : IsDomain R] →
[NeZero r] → e.Coprime r → { x // x ∈ primitiveRoots r R } ≃ { x // x ∈ primitiveRoots r R } :=
fun {R} {e r} [CommRing R] [IsDomain R] [NeZero r] h ↦
have coprmGcdA := equiv_primitiveRoots_of_coprimePow._proof_4;
have de2 := ⋯;
have de := ⋯;
have hea := ⋯;
{ toFun := fun μh ↦ ⟨↑μh ^ e, ⋯⟩, invFun := fun νh ↦ ⟨↑νh ^ ((↑r * e.gcdA r + 1) * e.gcdA r).toNat, ⋯⟩, left_inv := ⋯,
right_inv := ⋯ }
Mario Carneiro (Jun 29 2025 at 19:56):
set_option pp.proofs true
Mario Carneiro (Jun 29 2025 at 19:56):
each of those is probably a proof_n
metakuntyyy (Jun 29 2025 at 19:56):
Yes, indeed
def equiv_primitiveRoots_of_coprimePow.{u_1} : {R : Type u_1} →
{e r : ℕ} →
[inst : CommRing R] →
[inst_1 : IsDomain R] →
[NeZero r] → e.Coprime r → { x // x ∈ primitiveRoots r R } ≃ { x // x ∈ primitiveRoots r R } :=
fun {R} {e r} [CommRing R] [IsDomain R] [NeZero r] h ↦
have coprmGcdA := equiv_primitiveRoots_of_coprimePow._proof_4;
have de2 := equiv_primitiveRoots_of_coprimePow._proof_5;
have de := equiv_primitiveRoots_of_coprimePow._proof_6;
have hea := equiv_primitiveRoots_of_coprimePow._proof_7 h de;
{ toFun := fun μh ↦ ⟨↑μh ^ e, equiv_primitiveRoots_of_coprimePow._proof_8 h μh⟩,
invFun := fun νh ↦
⟨↑νh ^ ((↑r * e.gcdA r + 1) * e.gcdA r).toNat, equiv_primitiveRoots_of_coprimePow._proof_9 h coprmGcdA de νh⟩,
left_inv := equiv_primitiveRoots_of_coprimePow._proof_10 h coprmGcdA de hea,
right_inv := equiv_primitiveRoots_of_coprimePow._proof_11 h coprmGcdA de hea }
metakuntyyy (Jun 29 2025 at 19:58):
So what does generate the _proof_* declarations. Does any have statement that has multiple usages create one?
Mario Carneiro (Jun 29 2025 at 19:58):
any usage of a proof inside a def
Aaron Liu (Jun 29 2025 at 20:00):
Sometimes it doesn't generate the ._proof_n, if your proof is too short satisfies some criteria I have not yet decoded
Mario Carneiro (Jun 29 2025 at 20:01):
you don't want it to get into a loop of extraction, so at least constant applications have to be excluded
Mario Carneiro (Jun 29 2025 at 20:02):
but on the whole it seems pretty aggressive about it
metakuntyyy (Jun 29 2025 at 20:02):
And inside a theorem? Running
#print IsPrimitiveRoot.coe_submonoidClass_iff
Gives
theorem IsPrimitiveRoot.coe_submonoidClass_iff.{u_7, u_8} : ∀ {k : ℕ} {M : Type u_7} {B : Type u_8}
[inst : CommMonoid M] [inst_1 : SetLike B M] [inst_2 : SubmonoidClass B M] {N : B} {ζ : ↥N},
IsPrimitiveRoot (↑ζ) k ↔ IsPrimitiveRoot ζ k :=
fun {k} {M} {B} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] {N} {ζ} ↦
Eq.mpr
(id
(congr (congrArg Iff (IsPrimitiveRoot.coe_submonoidClass_iff._proof_1_1 (↑ζ) k))
(IsPrimitiveRoot.coe_submonoidClass_iff._proof_1_1 ζ k)))
(Eq.mpr
(id
(congrArg (fun x ↦ x ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), ζ ^ l = 1 → k ∣ l)
(congr (congrArg And OneMemClass.coe_eq_one._proof_3)
(forall_congr fun l ↦ implies_congr OneMemClass.coe_eq_one._proof_3 (Eq.refl (k ∣ l))))))
Iff.rfl)
Aaron Liu (Jun 29 2025 at 20:02):
Well if it's inside a theorem then it's not inside a def
Mario Carneiro (Jun 29 2025 at 20:02):
no I think that was a tactic that decided to do it
Aaron Liu (Jun 29 2025 at 20:03):
Why is it _1_1?
Mario Carneiro (Jun 29 2025 at 20:03):
probably extracted from within proof_1?
metakuntyyy (Jun 29 2025 at 20:04):
I always had trouble understanding what those were as I couldn't click them in the infoview. But it's good to poke a little bit deeper into the system.
So those auxiliary constants are created by tactics and to satisfy loop extraction?
Mario Carneiro (Jun 29 2025 at 20:04):
you should be able to click them
Mario Carneiro (Jun 29 2025 at 20:04):
you can certainly #print them
Mario Carneiro (Jun 29 2025 at 20:05):
it's just to decrease the amount of stuff e.g. the compiler has to look through when compiling constants
metakuntyyy (Jun 29 2025 at 20:05):
I can hover over them, I can't click them. I can print them but I remember there was one issue where I couldn't even find the constant. I don't remember which tactic generated them but it might have been grind.
metakuntyyy (Jun 29 2025 at 20:06):
Would this be a bug worth reporting? If so I could try to find and reproduce it.
Mario Carneiro (Jun 29 2025 at 20:09):
coe_submonoidClass_iff._proof_1_1 is created by simp, it pre-applies propext to the user lemma iff_def in the call
Sebastian Ullrich (Jun 29 2025 at 20:36):
Mario Carneiro said:
Why are the distributed olean files reporting a pre-release version, and why is this not causing a version mismatch?
Ah, that doesn't look right. But only the githash is relevant for the compatibility check.
Last updated: Dec 20 2025 at 21:32 UTC