Email Gateway (Feb 12 2021 at 18:29): Email Gateway (Feb 12 2021 at 18:29):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.
Email Gateway (Feb 15 2021 at 09:16):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
Email Gateway (Feb 15 2021 at 12:20):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
Email Gateway (Feb 15 2021 at 13:36):From: Tobias Nipkow <nipkow@in.tum.de>
Jasmin,
Greatr work!
How exactly do you activate Zipperposition?
Tobias
smime.p7s
Last updated: Apr 19 2024 at 20:15 UTC