Email Gateway (Aug 18 2022 at 13:41): Email Gateway (Aug 18 2022 at 13:41):From: Makarius <makarius@sketis.net>
comment syntax. It depends on the Emacs version how they interact or
nest, but most of the time it will just break down.
The deeper problem is manifold. XEmacs is hardly maintained anymore, and
Proof General support of it is diminished in recent PG 3.7.x versions.
In PG 4.0, if it is ever released, there will be only support for recent
GNU Emacsen.
Makarius
Email Gateway (Aug 18 2022 at 13:42):From: Makarius <makarius@sketis.net>
This problem is inherited from Debian, and already many years old. It
seems that Debian maintainers are busy elsewhere ...
I used to have my own XEmacs 21.4.20 (or similar) compiled manually on
Ubuntu. More recently I no longer managed to make it work, and started
using the GNU Emacs 22 GTK included in Ubuntu.
Makarius
Email Gateway (Aug 18 2022 at 13:42):From: Christian Urban <urbanc@in.tum.de>
Makarius writes:
BTW, since Christian Urban (who is managing the IDP) is always hooked on
some repository version, readers of the "current" tutorial will need to
learn both Isabelle internals and the very delicate internal development
process at the same time.
The use of "current" for the Programming Tutorial is
not set in stone. As Markus implied, following "current" has
its disadvantages. It is the most convenient for me at the
moment. If contributors of the Tutorial complain enough, I
am sure I will bend over backwards to accommodate their views.
As far as readers are concerned, the difference is mostly
syntactic nature
stable: current:
makestring -> PolyML.makestring
import_thms -> import
NamedThmsFun -> Named_Thms
DatatypePackage.get_datatype -> Datatype.get_info
tctical.ML -> tactical.ML
inductive_package.ML -> inductive.ML
If the ride gets bumpier, I will think of something.
Best wishes,
Christian
Email Gateway (Aug 18 2022 at 13:42):From: Makarius <makarius@sketis.net>
These are just some superficial things that are detected when recompiling
the tutorial. The main point is that a development snapshot is more or
less undefined, with many potential problems lurking. (Of course I know
many of them right now. Proper consolidation will take place for official
releases, and usually takes about 6-8 weeks.)
Maybe Christian can point out a version (with changeset id) of the
programming tutorial that works with the real Isabelle2009 version.
Makarius
Email Gateway (Aug 18 2022 at 13:42):From: Christian Urban <urbanc@in.tum.de>
Makarius writes:
Maybe Christian can point out a version (with changeset id) of the
programming tutorial that works with the real Isabelle2009 version.
Yes, of course I can do that to whomever wants to have this
information (this needs a bit digging and testing). Just send
me an email. I made also a similar pointer on the webpage.
Best wishes,
Christian
Email Gateway (Aug 18 2022 at 13:52):From: Christian Doczkal <doczkal@ps.uni-sb.de>
Hello
If I open Emacs/ProofGeneral and load todays version of "FirstSteps.thy"
and scroll down emacs just hangs (100% CPU, no reaction for minutes,
sometimes it comes back). If I disable font-lock mode this problem
disappears. No Isabelle process running at this time
I suspect this has something to do with the antiquotations in the text
blocks. I had similar problems before but only with antiquotations whose
parenthesis do not match.
Loosely related: There seems to be an error in the text block beginning
at in lines 978-1009. Isabelle (yesterdays development snapshot) refused
to check this block with error message:
*** Outer lexical error: missing end of verbatim text at Unfort ...
*** Outer syntax error: document source expected,
*** but bad input {* was found
*** Outer lexical error: missing end of verbatim text at Unfort ...
*** Outer lexical error: bad input at \emph{not} ...
*** Outer lexical error: bad input at \mbox{@{te ...
*** missing quote at end of string at (@; \<^sync>;
If I remove this text block isabelle checks the document without errors,
but the ProofGerenal/font-lock-mode problem persists.
I use Emacs (22.2.1) and ProofGeneral (3.7.1) on Ubuntu 9.04 AMD64. Can
someone reproduce this error? Is there a workaround except disabling
font-lock-mode?
Email Gateway (Aug 18 2022 at 13:52):From: Makarius <makarius@sketis.net>
This is a known problem of Proof General 3.7.1 running on GNU Emacs.
Maybe this helps:
http://www4.in.tum.de/~wenzelm/cgi-bin/repos.cgi/ProofGeneral/rev/36eccb23fddf
Anyway, what is "todays version of FirstSteps.thy"? I have never heard of
such a file in the Isabelle repository. "Yesterdays development snapshot"
is also hard to pin down.
With distributed version control (Mercurial), one needs to refer to
versions via the official id -- commit dates don't count. In Isabelle
development snapshots this is printed as "welcome" message of
isabelle-process or by "isabelle version".
Or you can just refer to the full URL, e.g. via the link on
http://isabelle.in.tum.de/devel which happens to be
http://isabelle.in.tum.de/repos/isabelle/changelog/f01207d56583 right now.
As usual, one needs to have very strong reasons to "use" a development
snapshot instead of a proper release. In particularly, one needs to keep
an eye on the Mercurial history all the time.
Makarius
Email Gateway (Aug 18 2022 at 13:52):From: Christian Doczkal <c.doczkal@stud.uni-saarland.de>
Thanks a lot Makarius
This is a known problem of Proof General 3.7.1 running on GNU Emacs.
Maybe this helps:http://www4.in.tum.de/~wenzelm/cgi-bin/repos.cgi/ProofGeneral/rev/36eccb23fddf
This did indeed solve the problem (merely changing this single file in
PG 3.7.1.
Anyway, what is "todays version of FirstSteps.thy"? I have never heard of
such a file in the Isabelle repository. "Yesterdays development snapshot"
is also hard to pin down.
OK, I should have been more precise. I was referring tho the file
"FirstSteps.thy" from the Isabelle Documentation Project.
With distributed version control (Mercurial), one needs to refer to
versions via the official id -- commit dates don't count. In Isabelle
development snapshots this is printed as "welcome" message of
isabelle-process or by "isabelle version".
I was referring to:
Isabelle repository snapshot 228905e02350 (23-Jul-2009)
But with font-lock-mode working again it was easy to spot the mistake.
There is only a space missing in "FirstSteps.thy". (diff attached,
referring to rev d6e9fb662d68, in case someone from the IDP reads this)
Thanks a lot, so now I can continue trying to understand the Isabelle
internals.
Have a nice weekend.
FirstSteps.diff
smime.p7s
Email Gateway (Aug 18 2022 at 13:52):From: Christian Urban <urbanc@in.tum.de>
Hi Christian,
Christian Doczkal writes:
But with font-lock-mode working again it was easy to spot the mistake.
There is only a space missing in "FirstSteps.thy". (diff attached,
referring to rev d6e9fb662d68, in case someone from the IDP reads this)
< \mbox{@{text "(op *)"}}:
\mbox{@{text "(op * )"}}:
I am not sure whether this is also a problem with Emacs
and parsing of comments. It is possible to write
@{text "(op * )"}
but it produces an ugly space in front of the parenthesis,
which I would like to avoid. My Xemacs does not choke on
the original
@{text "(op *)"}
Would you be able to test, for example by trying out different
emacses, where the problem comes from?
Thanks,
Christian
Email Gateway (Aug 18 2022 at 13:52):From: Christian Urban <urbanc@in.tum.de>
Makarius writes:
With distributed version control (Mercurial), one needs to refer to
versions via the official id -- commit dates don't count. In Isabelle
development snapshots this is printed as "welcome" message of
isabelle-process or by "isabelle version".
In case of the programming tutorial, the Isabelle version that
is used for producing the pdf is printed at the end of the
Introduction (though this might not have worked lately; it
works now again). The repository is at
http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/isabelle-cookbook
Christian
Email Gateway (Aug 18 2022 at 13:52):From: Christian Urban <urbanc@in.tum.de>
Christian Doczkal writes:
My Xemacs does not choke on
the original@{text "(op *)"}
Neither does (my) isabelle make
(Isabelle repository snapshot 228905e02350 (23-Jul-2009))
This very much hints at a problem with Emacs/ProofGeneral,
since when invoked via make the source code is directly
fed into Isabelle. In the file below, all incarnations
of "(op *)" are valid instances of Isabelle input. Maybe
this helps to find out what the problem is.
Christian
Times.thy
Email Gateway (Aug 18 2022 at 13:52):From: Christian Doczkal <c.doczkal@stud.uni-saarland.de>
Dear Christian Urban
I am not sure whether this is also a problem with Emacs
and parsing of comments. It is possible to write@{text "(op * )"}
but it produces an ugly space in front of the parenthesis,
which I would like to avoid. My Xemacs does not choke on
the original@{text "(op *)"}
Neither does (my) isabelle make
(Isabelle repository snapshot 228905e02350 (23-Jul-2009))
Would you be able to test, for example by trying out different
emacses, where the problem comes from?
I tried but the XEmacs package on Ubuntu seems to be totally broken.
smime.p7s
Email Gateway (Aug 18 2022 at 13:53):From: Christian Doczkal <c.doczkal@stud.uni-saarland.de>
OK, some tests:
of "(op *)" are valid instances of Isabelle input. Maybe
this helps to find out what the problem is.
ML {*
(op *)
*}
*** Outer lexical error: missing end of verbatim text at (op *) ...
*** Outer syntax error: ML source expected,
*** but bad input {* was found
*** Outer lexical error: missing end of verbatim text at (op *) ...
I can't really make sense of the error message
text {* @{text "(op *)"} *}
I can't see any complete commands to process!
Remark: everything following in the theory file (except antiquotations)
is highlighted in the same color as HOL Terms (just as "%x. x" in term
"%x. x")
text {* s @{term {*(op )} } foo *}
*** missing closing brace of antiquotation at term {*(op ...
*** At command "text".
Remark: Cursor jumps to the "}" right before the foo
Considering the second and the fact that it seems to work in XEmacs my
question would be whether PG relies on emacs parsing to determine what
part of the theory to send to the isabelle process? (I have no clue how
this works)
I hope this helps
Can someone reproduce this?
smime.p7s
Email Gateway (Aug 18 2022 at 13:53):From: Makarius <makarius@sketis.net>
OK, now I get the idea.
BTW, since Christian Urban (who is managing the IDP) is always hooked on
some repository version, readers of the "current" tutorial will need to
learn both Isabelle internals and the very delicate internal development
process at the same time.
Makarius
Last updated: May 03 2024 at 08:18 UTC