Email Gateway (Aug 22 2022 at 19:50): Email Gateway (Aug 22 2022 at 19:50):From: Peter Lammich <lammich@in.tum.de>
Hi List,
an initial experiment on porting my current ~42kLOC project from
2018 to RC2 went surprisingly well.
I only encountered a few changes not explicitly covered by NEWS:
* There are various renamings in HOL-Words, and maybe also simpset
changes (?). This is not explicitly mentioned by the NEWS entry.
* The ML-Level interface of intro_locales_tac changed. The new
"strict" and "eager" flags are not documented at all, I figured out
the right combination for me by trial and error.
* Finally, the option Syntax_Trans.eta_contract_raw disappeared. Its
now just eta_contract, and properly typed!
* A few proofs involving {auto,fastforce} and combinations of split:
and split!: stopped to work, and had to be re-done more explicitly. I
have not figured out the exact reason.
* My project involves a custom code generator. I am still using an
implementation that I adapted from the 2018 standard code generator for
generating files relative to the theory folder. This still works, but I
understand that I have to port it to the new VFS idiom.
The following (already reported) issues remain:
* The fonts still look more blurry than in 2018, on my full HD screen
* The NEWS file does not specify any replacement for old style inner
comments (* *). The entry for Isabelle-2018 says to use \comment or
\cancel. However, content of \comment is interpreted as latex text,
causing trouble with unknown antiquotations when e.g. trying to comment
out "{1,2}@{a,b}". Moreover, \cancel used to occur in "striked out"
style in Latex output, at least when used in outer syntax. Is this also
the case for inner-syntax \cancel? Can I make parts of inner syntax
disappear from latex output?
Best,
Peter
Email Gateway (Aug 22 2022 at 19:51):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
* There are various renamings in HOL-Words, and maybe also simpset
changes (?). This is not explicitly mentioned by the NEWS entry.
this relates to a post of mine on this mailing list from May 3rd:
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. * Other theories in HOL-Word have undergone a massive internal
re-structuring and re-grouping of material, absorbing material from AFP
sessions, particulary Native_Word.
The mere amount of material plus the absence of any deliberate change
made it difficult to distill a conclusive NEWS entry from that. But if
you have specific observations (e. g. reoccurring proof-breaking
patterns), I am happy to mention them there (or maybe amend HOL-Word
accordingly).
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 19:53):From: Makarius <makarius@sketis.net>
The relevant change for Locale.intro_locales_tac is here:
https://isabelle.sketis.net/repos/isabelle-release/rev/0c1d7a414185 --
it should make clear how to upgrade this rarely used operation.
(Recall that the outdated terminology of "ML-level" is leading to
misunderstandings about the true structure of Isabelle. It should be
possible to get rid of it eventually, 10 years after it became out of
proper use.)
Makarius
Email Gateway (Aug 22 2022 at 19:53):From: Makarius <makarius@sketis.net>
We've had that already: Java 11 font rendering is more honest -- good on
good displays, and bad on bad displays.
The Isabelle/jEdit manual has some further explanations on that:
https://isabelle.sketis.net/repos/isabelle-release/file/be248d734a5d/src/Doc/JEdit/JEdit.thy#l364
https://isabelle.sketis.net/repos/isabelle-release/file/be248d734a5d/src/Doc/JEdit/JEdit.thy#2150
The latter are explicit instructions to downgrade to old Java 8
(end-of-life since Jan-2019).
Makarius
Email Gateway (Aug 22 2022 at 19:53):From: Makarius <makarius@sketis.net>
On 19/05/2019 19:09, Makarius wrote:
On 14/05/2019 13:46, Peter Lammich wrote:
The following (already reported) issues remain:
* The fonts still look more blurry than in 2018, on my full HD screenWe've had that already: Java 11 font rendering is more honest -- good on
good displays, and bad on bad displays.The Isabelle/jEdit manual has some further explanations on that:
[proper links]
https://isabelle.sketis.net/repos/isabelle-release/file/be248d734a5d/src/Doc/JEdit/JEdit.thy#l364
https://isabelle.sketis.net/repos/isabelle-release/file/be248d734a5d/src/Doc/JEdit/JEdit.thy#l2150
The latter are explicit instructions to downgrade to old Java 8
(end-of-life since Jan-2019).
Makarius
Email Gateway (Aug 22 2022 at 19:53):From: Makarius <makarius@sketis.net>
On 14/05/2019 13:46, Peter Lammich wrote:
* The NEWS file does not specify any replacement for old style inner
comments (* *). The entry for Isabelle-2018 says to use \comment or
\cancel. However, content of \comment is interpreted as latex text,
causing trouble with unknown antiquotations when e.g. trying to comment
out "{1,2}@{a,b}". Moreover, \cancel used to occur in "striked out"
style in Latex output, at least when used in outer syntax. Is this also
the case for inner-syntax \cancel?
Old style inner comments were not really well-defined, and treated
differently from outer comments (which are like % in LaTeX).
The purpose of the reform of formal comments was to make it all work
uniformly, e.g. see the included example.
Can I make parts of inner syntax disappear from latex output?
Is that a new feature request for Isabelle2020?
In Isabelle2019 you can try with the low-level \<^latex> operator, but
it is a bit awkward and fragile. For example:
term ‹x\<^latex>‹%ignored @{text}
››
Makarius
Test.thy
document.pdf
Email Gateway (Aug 22 2022 at 19:54):From: Makarius <makarius@sketis.net>
Here is again the Test.thy with its document.pdf -- the makers of
Thunderbird seem to believe in Physics more than Mathematics: when
updating an attached file in the file-system, its updated version is
sent out.
Makarius
Test.thy
document.pdf
Last updated: Apr 26 2024 at 08:19 UTC