Email Gateway (Aug 22 2022 at 19:46): Email Gateway (Aug 22 2022 at 19:46):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
recently I had a closer look at the session HOL-Word; what started as a
mere analysis out of curiousity turned into a substantial overhaul of
existing material resulting in a plan for the time after the next release.
What is relevant for the next release:
The traditional entry point HOL-Word.Word is supposed to be
meta-stable: there might be issues due to things like additional simp
rules and oscillating full theorem names etc. as not uncommon for new
releases, but there are no intentional changes in scope there.
HOL-Word.More_Word is an additional »sumo« enty point into HOL-Word.
Some time after the release I would attempt a de-baroquification
(purification?) of HOL-Word: there is evidence that the essentially
needed things can be expressed quite compactly using state-of-the-art
tools in Isabelle/HOL; preliminary case studies can be found in
src/HOL/ex/Bit_Lists.thy and src/HOL/ex/Word_Type.thy (which are just a
start, there is much more in the pipeline). Hence I hope that in the
long run bit and word types and operations can take place in two
theories in HOL-Library, which HOL-Word that just builds upon; we will
see which applications then still need full HOL-Word.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 19:46):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
Hi Florian,
I think that is a good endeavour, there is indeed much that can be expressed more nicely these days. Keeping larger changes to after Isabelle2019 would be good.
For testing, I guess we are one of the biggest users of Word proofs, so it might make sense to have a look at https://github.com/seL4/l4v/ and run that for at least the ARM architecture settings. Of course this is on Isabelle2018. There is another round of material accumulated there that I was planning to contribute to the AFP Word entry before the Isabelle2019 release, but I will probably run out of time (project deadlines, haven’t even managed yet to test RC1) and have to move it to the next one.
Are your current HOL-Word changes already in RC1 or planned for RC2? Was there much impact on AFP.Word_Lib?
I’m also happy to help with testing later changes and be involved in the content evolution of HOL-Word.
Cheers,
Gerwin
Email Gateway (Aug 22 2022 at 19:46):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Gerwin,
I think that is a good endeavour, there is indeed much that can be expressed more nicely these days. Keeping larger changes to after Isabelle2019 would be good.
For testing, I guess we are one of the biggest users of Word proofs, so it might make sense to have a look at https://github.com/seL4/l4v/ and run that for at least the ARM architecture settings. Of course this is on Isabelle2018. There is another round of material accumulated there that I was planning to contribute to the AFP Word entry before the Isabelle2019 release, but I will probably run out of time (project deadlines, haven’t even managed yet to test RC1) and have to move it to the next one.
Are your current HOL-Word changes already in RC1 or planned for RC2? Was there much impact on AFP.Word_Lib?
the changes are already there in RC1. The impact on AFP entries is
minimal. In fact the primary purpose of the reorganization was to
understand what the fundamental concepts are and group the material
accordingly.
I’m also happy to help with testing later changes and be involved in the content evolution of HOL-Word.
My aim is to leave HOL-Word.Word more or less »as it is«, but basing it
on newly emerging theories; this would allow to gradually find out which
parts of HOL-Word.Word are obsolete for particular applications without
endangering those that still need it.
Cheers,
Florian
signature.asc
Last updated: Apr 18 2024 at 04:17 UTC