Email Gateway (Aug 23 2022 at 08:51): Email Gateway (Aug 23 2022 at 08:51):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
the Isabelle2020 release process is approaching its end: a really final and
immutable version will be published on 15-Apr-2020.
Here is one more pre-final approximation of that, with a small change for
Sledgehammer: https://isabelle.in.tum.de/website-Isabelle2020-RC5
See again the blog entry
https://isabelle-dev.sketis.net/phame/post/view/5/release_candidates_for_isabelle2020
for further details all changes so far.
When discussing observations about Isabelle2020 release candidates on the
mailing list, please provide a "Subject:" line that fits to the content, not
just a clone of this announcement.
Makarius
Email Gateway (Aug 23 2022 at 08:52):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,
While porting some of my previous work to RC4, I noticed what to me seems
to be a minor discrepancy in one of the NEWS entries (the entry is the same
in RC5 according to
https://isabelle.in.tum.de/website-Isabelle2020-RC5/dist/Isabelle2020-RC5/doc/NEWS.html
):
If I am not mistaken, in Isabelle 2019 there exists the component
auto_fixes in the structure Variable, but there is no component auto_fixes
in the structure Proof_Context. Perhaps, Proof_Context.augment in
Isabelle2020 is meant to replace Variable.auto_fixes in Isabelle2019? Even
if I am not mistaken, please accept my apologies for being overly picky.
Kind Regards,
Mikhail Chekhov
Email Gateway (Aug 23 2022 at 08:52):From: Peter Lammich <lammich@in.tum.de>
Hi,
I ran into the same issue. I simply replaced my Variable.auto_fixes by
Proof_Context.augment, but without really knowing what I'm doing ;)
Email Gateway (Aug 23 2022 at 08:53):From: Makarius <makarius@sketis.net>
Thanks, I have fine-tuned it here:
https://isabelle.sketis.net/repos/isabelle-release/rev/f39b1afe8845
Since the NEWS file is not formally checked, there can always be minor
deviations from the reality in the repository.
Moreover, it is often required to go back several releases in the NEWS, and
mentally translate what was told some years ago into the present context.
Makarius
Email Gateway (Aug 23 2022 at 08:53):From: Peter Lammich <lammich@in.tum.de>
Hi,
just in the middle of my work, I was interrupted by a "Prover process
terminated with error" dialogue displaying the message below. I think I
was just switching to another theory file, that was already open.
(I've never seen a message like this. The last time I saw something
similar was when using ProofGeneral and it got out of sync with
Isabelle)
Peter
Welcome to Isabelle/HOL (Isabelle2020-RC5: April 2020)
Interrupt
Interrupt
Interrupt
standard_error terminated
standard_output terminated
process terminated
Malformed message:
bad chunk (unexpected EOF after 679 of 836 bytes)
message_output terminated
command_input terminated
process_manager terminated
Return code: 137
On the command line, I see
j65266pl@cspool450:~/devel/isabelle/RF2/llvm$ ~/opt/Isabelle2020-
RC5/bin/isabelle jedit -d ~/devel/isabelle/afp-devel/thys/
basic/LLVM_Basic_Main.thy
12:57:53 [Session.manager] [error] manager: ### Ignored report message:
<completion offset="51" end_offset="56"
id="508"><:>1</:><:><:><:>LLVM_Monad</:><:><:>theory</:><:>LLVM_Monad</
:></:></:></:></completion>
12:57:54 [Session.manager] [error] manager: ### Ignored report message:
<completion offset="51" end_offset="56"
id="514"><:>1</:><:><:><:>LLVM_Monad</:><:><:>theory</:><:>LLVM_Monad</
:></:></:></:></completion>
13:35:29 [Session.manager] [error] manager: ### Ignored report message:
<completion offset="86" end_offset="95"
id="94448"><:>1</:><:><:><:>More_Word_RF2</:><:><:>theory</:><:>More_Wo
rd_RF2</:></:></:></:></completion>
13:35:31 [Session.manager] [error] manager: ### Ignored report message:
<completion offset="86" end_offset="97"
id="94454"><:>1</:><:><:><:>More_Word_RF2</:><:><:>theory</:><:>More_Wo
rd_RF2</:></:></:></:></completion>
13:35:58 [Session.manager] [error] manager: ### Ignored report message:
<completion offset="86" end_offset="95"
id="94822"><:>1</:><:><:><:>RF2_More_Word</:><:><:>theory</:><:>RF2_Mor
e_Word</:></:></:></:></completion>
13:35:59 [Session.manager] [error] manager: ### Ignored report message:
<completion offset="86" end_offset="97"
id="94828"><:>1</:><:><:><:>RF2_More_Word</:><:><:>theory</:><:>RF2_Mor
e_Word</:></:></:></:></completion>
On Wed, 2020-04-08 at 14:32 +0200, Makarius wrote:
Dear Isabelle users,
the Isabelle2020 release process is approaching its end: a really
final and
immutable version will be published on 15-Apr-2020.Here is one more pre-final approximation of that, with a small change
for
Sledgehammer: https://isabelle.in.tum.de/website-Isabelle2020-RC5See again the blog entry
https://isabelle-dev.sketis.net/phame/post/view/5/release_candidates_for_isabelle2020
for further details all changes so far.When discussing observations about Isabelle2020 release candidates on
the
mailing list, please provide a "Subject:" line that fits to the
content, not
just a clone of this announcement.Makarius
Last updated: Apr 19 2024 at 01:05 UTC