From: Peter Lammich <lammich@in.tum.de>
Hi List.
I have now ported a big chunk of Isabelle-LLVM to RC5.
Notably, Isabelle-LLVM extensively uses the Word library, and also
contains some lower-level Isabelle-ML code.
First, Isabelle seems to run stable. I did not run into any
unrecoverable grey-out.
It was killed one time by my OOM killer, but I had two instances in
parallel on 32GB RAM.
With the NEWS file, and a bit of guessing, the Isabelle-ML code was
easily ported, most severe problem was the undocumented change
Path.smart_implode -> Path.implode_symbolic.
Porting of lemmas using the word library was, as expected, more
difficult. With the help of sledgehammer, which feels really powerful,
I could force most lemmas through, even without a complete
understanding or overview of the changes to Word.
From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Peter,
You wrote:
If Sledgehammer feels more powerful, it's because it is. Makarius has repackaged many of the provers, using the latest versions; this was long overdue. On the Sledgehammer side, Martin has been doing the necessary integration, testing, and evaluation work. I'm very grateful to both! The integration of veriT as a reconstruction method, by Hans-Jörg, Mathias, and Martin, also helps reduce reconstruction failures by half, they claim in their draft [*]. Two more highlights:
We now communicate with E in a lambda-free HOL logic with support for currying and Booleans. That helps the success rate a lot. (E should get lambdas and HO unification this year.)
Sledgehammer now includes the Zipperposition higher-order prover that's developed largely by my team. It won last year CASC's higher-order division by a record margin. It's not enabled by default because we ran out of time to test it thoroughly, but you can add it to the Sledgehammer panel or "sledgehammer_params". It's good on HO things like p {x. q x | r x} ==> p {x. r x | q x} (which should be trivial but are "lost in translation" to FOL). Reconstruction remains a challenge, though.
Jasmin
[*] https://matryoshka-project.github.io/pubs/verit_isa_paper.pdf
From: Lawrence Paulson <lp15@cam.ac.uk>
These are great developments! But already, for some years now, sledgehammer has been good enough to help people prove things they didn’t really understand. That’s how I managed to port tens of thousands of lines of incomprehensible HOL Light proofs. It’s also good at discovering contradictions when people have been using “sorry” a little too freely.
It’s not fanciful to foresee a “self-healing” capability for proof developments: where you update a definition and the system would identify and automatically repair proofs that broke as a result. Also in the not-too-distant future might be source to source translations of structured proofs from one proof assistant to another, with high-level proofs in the target system being generated automatically using the source proofs as hints (as opposed to the current practice of emulating one formalism within another).
Larry
From: Tobias Nipkow <nipkow@in.tum.de>
Jasmin,
Greatr work!
How exactly do you activate Zipperposition?
Tobias
smime.p7s
Last updated: Jan 25 2022 at 01:11 UTC