Email Gateway (Feb 04 2025 at 13:28): Email Gateway (Feb 04 2025 at 13:28):From: Fabian Huch <huch@in.tum.de>
There are a few small problems in the documentation: They aren't new
regressions, but could be improved for the release.
doc/sugar.pdf: text_raw {*
doc/sugar.pdf: text_raw {*
doc/sugar.pdf: \text_raw{\snip{snippetname}{1}{2}{%}
doc/sugar.pdf: \text_raw{}%endsnip}
doc/logics-ZF.pdf:by (tactic {IntPr.fast_tac 1})
doc/sugar.pdf: -- "pretty trivial"
The old tutorial contains more outdated syntax, but that is probably
expected.
Fabian
On 2/3/25 20:22, Makarius wrote:
Dear Isabelle users,
we are now ready to start the release process for Isabelle2025 (March
2025). See also the continuously updated blog entry
https://isabelle-dev.sketis.net/phame/post/view/85/release_candidates_for_isabelle2025The current release candidate is available from
https://isabelle.in.tum.de/website-Isabelle2025-RC1A corresponding version of the Archive of Formal Proofs is
https://isabelle.sketis.net/repos/afp-devel/rev/634f3bc5f94bThe NEWS and ANNOUNCE files are already up-to-date, but some
documentation still requires update.The rules of the game are the same as in the past few decades: NOW is
the window of opportunity to discuss observations and problems, in
order to get changes into the code-base. The final release remains
unchangeable, until the next one (8-10 months later).Any feedback about Isabelle release candidates should be posted with a
meaningful Subject, not just a clone of this announcement.Makarius
Email Gateway (Feb 04 2025 at 14:26):From: "John F. Hughes" <jfh@cs.brown.edu>
Also, in two of the lines Fabian noted, namely
doc/sugar.pdf: \text_raw{\snip{snippetname}{1}{2}{%}
doc/sugar.pdf: \text_raw{}%endsnip}
there should not be a backslash before the "text_raw", even after the
comments have been changed to new-style.
--John
On Tue, Feb 4, 2025 at 8:28 AM Fabian Huch <huch@in.tum.de> wrote:
There are a few small problems in the documentation: They aren't new
regressions, but could be improved for the release.
- old-style block quotes ("{* ... *}") that no longer work:
doc/sugar.pdf: text_raw {*
doc/sugar.pdf: text_raw {*
doc/sugar.pdf: \text_raw{\snip{snippetname}{1}{2}{%}
doc/sugar.pdf: \text_raw{}%endsnip}
doc/logics-ZF.pdf:by (tactic {IntPr.fast_tac 1})
- old-style comments (' -- "..." ') that no longer work:
doc/sugar.pdf: -- "pretty trivial"
- Extra parameter in rail diagram (doc/isar-ref.pdf): try0 and
sledgehammer have a trailing nat parameter, which does not actually
exist (as far as I can tell).The old tutorial contains more outdated syntax, but that is probably
expected.Fabian
On 2/3/25 20:22, Makarius wrote:
Dear Isabelle users,
we are now ready to start the release process for Isabelle2025 (March
2025). See also the continuously updated blog entry
https://isabelle-dev.sketis.net/phame/post/view/85/release_candidates_for_isabelle2025The current release candidate is available from
https://isabelle.in.tum.de/website-Isabelle2025-RC1A corresponding version of the Archive of Formal Proofs is
https://isabelle.sketis.net/repos/afp-devel/rev/634f3bc5f94bThe NEWS and ANNOUNCE files are already up-to-date, but some documentation
still requires update.The rules of the game are the same as in the past few decades: NOW is the
window of opportunity to discuss observations and problems, in order to get
changes into the code-base. The final release remains unchangeable, until
the next one (8-10 months later).Any feedback about Isabelle release candidates should be posted with a
meaningful Subject, not just a clone of this announcement.Makarius
Email Gateway (Feb 06 2025 at 21:27):From: Makarius <makarius@sketis.net>
On 04/02/2025 14:28, Fabian Huch wrote:
- Extra parameter in rail diagram (doc/isar-ref.pdf): try0 and sledgehammer
have a trailing /nat/ parameter, which does not actually exist (as far as I
can tell).
I am only responsible for this one. See now
https://isabelle-dev.sketis.net/rISABELLEdf68d656d5c4
There is indeed no proof in the history that 'try0' ever had this optional nat
argument.
In contrast, sledgehammer has it, as optional subgoal number. (It might have
been forgotten over time). Example:
lemma False and True
sledgehammer run 2
(Try this: prefer 2 apply simp)
The old tutorial contains more outdated syntax, but that is probably expected.
It is in the documentation section "Old Isabelle Manuals". It should be clear
that old manuals are outdated.
Over many years, I made a continuous effort to move things from the former
"ref" manual into "isar-ref" and "implementation" --- while staying in remote
areas with laptop + bycicle only (no network). I never ventured into the other
manuals, though.
Maybe Larry wants to rewrite his old "intro" manual to fit into the current
system: I've found that a very valuable document in 1994. It could be
refreshed with material from his more recent blog.
Makarius
Email Gateway (Feb 08 2025 at 16:46):From: Fabian Huch <huch@in.tum.de>
On 2/6/25 22:27, Makarius wrote:
On 04/02/2025 14:28, Fabian Huch wrote:
- Extra parameter in rail diagram (doc/isar-ref.pdf): try0 and
sledgehammer have a trailing /nat/ parameter, which does not actually
exist (as far as I can tell).I am only responsible for this one. See now
https://isabelle-dev.sketis.net/rISABELLEdf68d656d5c4
Great, thank you!There is indeed no proof in the history that 'try0' ever had this
optional nat argument.In contrast, sledgehammer has it, as optional subgoal number. (It
might have been forgotten over time). Example:lemma False and True
sledgehammer run 2
(Try this: prefer 2 apply simp)
I see, I missed the "run" mode here.
Fabian
Last updated: Mar 09 2025 at 12:28 UTC