Email Gateway (Jul 27 2023 at 10:25): Email Gateway (Jul 27 2023 at 10:25):From: Peter Lammich <lammich@in.tum.de>
Porting of Isabelle-LLVM from 2022 to 2023-RC2 went ahead without major
issues.
Only minor things that were not covered by NEWS:
* Morphism.entity seems to be a new concept, at least it's needed in
some places where e.g. Morphism.thm used to be enough
* Path.implode_symbolic no longer exists. Is it safe to be replaced by
Path.implode?
* Local_Theory.declaration now takes a pos argument. I blindly
followed an example from AFP, and used "\^here", but don't know what
it's actually good for. In AFP, all occurrences have simply been
amended with ^here, in the Isabelle sources, some use ^here, and
others use "Binding.pos_of binding", 'forwarding' the position of
some binding.
Email Gateway (Jul 27 2023 at 18:40):From: Makarius <makarius@sketis.net>
On 27/07/2023 12:24, Peter Lammich wrote:
Porting of Isabelle-LLVM from 2022 to 2023-RC2 went ahead without major issues.
Thank you for testing. It is important to substantiate the claim that we are
approaching a proper release.
* Morphism.entity seems to be a new concept, at least it's needed in some
places where e.g. Morphism.thm used to be enough
I've put it on the list of things that will be potentially documented before
final lift-off. (Presently a lot of documentation details are missing.)
* Path.implode_symbolic no longer exists. Is it safe to be replaced by
Path.implode?
"hg grep --all" quickly reveals changeset a004c5322ea4, which shows a renaming
of Path.implode_symbolic to File.symbolic_path.
The concept of "symbolic" path it not properly documented anywhere (I think),
but it is becoming increasingly important for persistent session information
--- in SQLite db files or PostgreSQL database content.
It is irrelevant, if you merely build sessions locally for yourself, without
moving things elsewhere later on.
* Local_Theory.declaration now takes a pos argument. I blindly followed an > example from AFP, and used "\^here", but don't know what it's actually
good for. In AFP, all occurrences have simply been amended with ^here, in
the Isabelle sources, some use ^here, and others use "Binding.pos_of
binding", 'forwarding' the position of some binding.
This is a device for tracing / debugging of little relevance. Just use inline
\<^here> (funny "home" or "house" symbol).
Makarius
Last updated: Apr 28 2024 at 16:17 UTC