Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Empty session_graph files

Email Gateway (Aug 22 2022 at 13:08):

From: Fleury Mathias <mathias.fleury12@gmail.com>
Hello all,

while browsing some theory documentation, I noticed that the session_graph files (labeled "theory dependency" in the documentation) are empty (see for example http://isabelle.in.tum.de/dist/library/HOL/HOL/session_graph.pdf <http://isabelle.in.tum.de/dist/library/HOL/HOL/session_graph.pdf> or http://afp.sourceforge.net/browser_info/current/AFP/Jinja/session_graph.pdf <http://afp.sourceforge.net/browser_info/current/AFP/PropResPI/session_graph.pdf> in the AFP). The Isabelle2015 versions are not empty (see http://isabelle.in.tum.de/website-Isabelle2015/dist/library/HOL/HOL/session_graph.pdf <http://isabelle.in.tum.de/website-Isabelle2015/dist/library/HOL/HOL/session_graph.pdf> or http://afp.sourceforge.net/browser_info/Isabelle2015/AFP/Jinja/session_graph.pdf <http://afp.sourceforge.net/browser_info/Isabelle2015/AFP/Jinja/session_graph.pdf>).

Is this the expected behaviour?

Mathias

Email Gateway (Aug 22 2022 at 13:09):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi all,

I found the culprit (by bisecting the commits): it is commit http://isabelle.in.tum.de/reports/Isabelle/rev/dcc8e1d34b18 <http://isabelle.in.tum.de/reports/Isabelle/rev/dcc8e1d34b18> (by Makarius Wenzel). The change is simply:

• File.copy(graph_file, (session_prefix + Path.basic("session_graph.pdf")).file)
• File.write(session_prefix + Path.basic("session_graph.pdf"), File.read(graph_file))

Does anyone understand what is going on here? The two commands generates files with different sizes (File.write generates a longer file than File.copy).

Best regards,
Mathias

Email Gateway (Aug 22 2022 at 13:09):

From: Makarius <makarius@sketis.net>
Thanks for figuring out this drop-out from last October.

This is a typical Unicode accident: File.read and File.write operate on
type string in ML and String in Scala, but the latter only works for text
(in UTF8 encoding). Thus the non-text PDF is messed up.

So I need to go back to File.copy and ensure that reasonable file
permissions are produced by other means.

Makarius

Email Gateway (Aug 22 2022 at 13:29):

From: Joachim Breitner <breitner@kit.edu>
Hi,

I just noticed an empty session graph here as well, probably due to the
same reason.

Is there a way to get a session graph with Isabelle 2016 (without
applying a, eh, local code change to it)?

Greetings,
Joachim
signature.asc

Last updated: Apr 25 2024 at 08:20 UTC