oleans file could not be opened successfully

Stream: general

[Sky Wilshaw]

How can I purge local mathlib3 oleans? I think my local copy is broken, or I need to install an xz reader somehow.

Looking for mathlib oleans for 32a7e53528
  locally...
  Found local mathlib oleans
Located matching cache
Applying cache
file could not be opened successfully:
- method gz: ReadError('not a gzip file')
- method bz2: ReadError('not a bzip2 file')
- method xz: CompressionError('lzma module is not available')
- method tar: ReadError('invalid header')

[Scott Morrison]

Well, one good way to purge your mathlib3 oleans is to switch to using Lean 4. :-)

[Scott Morrison]

Sorry, I would have to go read the leanproject source at this point to remember where it stores things. Perhaps a more recent user of Lean 3 will be able to actually help. :-)

[Sky Wilshaw]

That's what I'm trying to do, haha! But I need to run mathport on lean 3 to get my lean 4 code.

[Scott Morrison]

It looks like the caches were stored in ~/.mathlib

[Scott Morrison]

If you don't mind having to redownload, it should be safe to just delete that directory.

[Sky Wilshaw]

I think my bigger issue at the moment is trying to use WSL2. I'll try the same procedure on an actual linux machine, I don't expect it to have this problem. Thanks!

[Sky Wilshaw]

(Everything froze...)

[Scott Morrison]

Feel free to ping me if you run into trouble. We do want to make sure people running mathport at project scale are not left behind!!

[Sky Wilshaw]

Thanks, I'll let you know how it goes! For context, I'm porting https://github.com/leanprover-community/con-nf

[Sky Wilshaw]

@Scott Morrison If you're interested, I've just finished porting the project. It came out to 12.4k LoC of Lean 4, translated from 12.2k LoC of Lean 3. I only ended up running mathport once, fixing all the little errors manually. Unsurprisingly mathport worked best on statements and proofs that exploited the kernel the least - things that didn't abuse defeqs, for example. I found that most of the time, it correctly guessed the case conventions of theorem
and definition statements, but often didn't propagate the name change to the uses of those theorems. In any case, the port only took a few days and everything's working just as well as it did back in Lean 3 - and a few of the more technical proofs are now rfl!

[Sky Wilshaw]

And CI is down from 20 mins to about 8! (not factorial)

[Sky Wilshaw]

Project page is https://leanprover-community.github.io/con-nf

[Patrick Massot]

Congratulations! What is the current status of this project? Are you making good progress in addition to porting to Lean 4? Do you think you are getting close to a full formalization?

[Sky Wilshaw]

Yes, I'm making good progress. I've proven the most important technical theorem of the project, the freedom of action theorem. It shows that there are a lot of permutations of the model in question (and moreover we can pick ones that have prescribed actions on small domains) and so the set of model elements can't be that large.

[Sky Wilshaw]

The Lean proof differs drastically from the paper proof - thousands of lines of code were needed to state and prove results that were just implicit in the paper.

[Sky Wilshaw]

The main issue is that every construction is wrapped in inductions inside inductions. On paper, you can pretty much claim whatever you like and appeal to well-foundedness, but in Lean you need to be careful about always referencing inductive hypotheses of the right form at the right time. The hardest part by far has been writing the statements of what is to be proven.

[Patrick Massot]

Sky Wilshaw said:

The hardest part by far has been writing the statements of what is to be proven.

I think this is pretty universal in formalized math, although it's probably worse than average in this specific project.