Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Consolidated Isabelle2018-RC2 available for te...

Email Gateway (Aug 22 2022 at 17:41):

From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Makarius,

I have encountered a minor snag with document preparation using a custom
"build" script (as commonly used for snippets). The build script never
generates a root.pdf file (only document.pdf), and producs an obscure
error:

isabelle document -d snippets/document -o pdf -n document
*** Error

The error appears to be the result of the following command

[ -f root.pdf ] && cp -f root.pdf ../document.pdf

which returns a non-zero exit code if root.pdf does not exist.

This can be traced to the build_document function in
src/Pure/present.scala, which does

bash("[ -f " + root_bash(document_format) + " ] && cp -f " +
root_bash(document_format) + " " + File.bash_path(document_target)).check

The .check here seems over-zealous.

(It's easy to work around the problem by generating root.pdf instead of
document.pdf)

Cheers,

Bertram

Email Gateway (Aug 22 2022 at 17:42):

From: Makarius <makarius@sketis.net>
On 25/07/18 15:19, Bertram Felgenhauer via Cl-isabelle-users wrote:

isabelle document -d snippets/document -o pdf -n document
*** Error

The error appears to be the result of the following command

[ -f root.pdf ] && cp -f root.pdf ../document.pdf

which returns a non-zero exit code if root.pdf does not exist.

This can be traced to the build_document function in
src/Pure/present.scala, which does

bash("[ -f " + root_bash(document_format) + " ] && cp -f " +
root_bash(document_format) + " " + File.bash_path(document_target)).check

Thanks for keeping an eye on such details.

The problem here is the boolean expression instead of a regular
if-statement. I have now amended that for the next release candidate:
https://isabelle.sketis.net/repos/isabelle-release/rev/71aa5a9128c2

The .check here seems over-zealous.

I've left that in, but changed the shell script instead. By default,
bash invocations under program control should be strict, to imitate the
normal evaluation of Isabelle/ML and Isabelle/Scala.

Makarius

Email Gateway (Aug 22 2022 at 17:53):

From: Makarius <makarius@sketis.net>
Dear Isabelle users,

the coming Isabelle2018 release is scheduled for August 2018, approx. 3
weeks from now. A consolidated release candidate is now available
for general testing: https://isabelle.in.tum.de/website-Isabelle2018-RC2
-- it is already forked off the main Isabelle repository, so very few
changes will happen until the final version.

The corresponding repository versions of Isabelle and AFP are
https://isabelle.sketis.net/repos/isabelle-release/rev/89e05bd572c6 and
https://bitbucket.org/isa-afp/afp-devel/commits/7175b64d54a4 respectively.

The website, NEWS, ANNOUNCE etc. are already up-to-date, but some
documentation still requires update.

The ongoing release process is continuously documented on my blog:
https://sketis.net/2018/release-candidates-for-isabelle2018

When discussing observations about release candidates, please provide
a mail Subject line that fits to the content, not just a clone of the
announcement.

The time for final testing and reporting pending problems is getting
very short now. After the release has been published, it is too late to
change anything (before the next release in approx. 10 months).

Makarius

Last updated: Nov 21 2024 at 12:39 UTC