Re: [isabelle] Easier quick PDF generation possible?

On Thu, 23 Oct 2014, Joachim Breitner wrote:

Here is my log:

1. run "isabelle mkroot"
2. notice that I ran it wrong, "rm ROOT"
3. run "isabelle mkroot -d"
4. add my theory to ROOT, removed the theories [document = false]
  section, because empty sections are not allowed
5. run "isabelle build -D"
6. noticed that a few other theories were pulled in that I did not want
7. tried to add their theory names to the [document = false] section,
  for which I first had to look up the syntax in another ROOT file
8. noticed that this did not work. Put in the theory path (i.e.
  "~~/src/HOL/Library/Extended_Real") in there
9. adjusted document/root.txt to have a proper title and not disclose my
  local username

Here is what I would have liked to do:

1. run "isabelle thy2pdf Foo.thy"

Note that Isabelle command-line tools are very old-fashioned, and many new things don't have a shell wrapper anymore. The direct way is via Isabelle/Scala. It is also possible to invoke Scala functionality in Isabelle/jEdit with the Console/Scala plugin.

This older thread gives some hints about document preparation via In Isabelle2014 this works a bit more smoothly, but there is still no direct IDE support.

So if anyone agrees that this would be useful, and is able to implement
this minor feature suggestion

Above you describe too missing things in the current PIDE setup:

  (1) management of "projects", i.e. sorting out ROOT files

  (2) document-preparation within the IDE

These are not "minor" things, but quite important. Both of that is in the pipeline for a long time. Last winter I tried hard to revisit point (2), but got entangled in old TTY / Proof General features. Since the latter has been cleared out at last, some more progress is to be expected eventually.


          777,071 people so far

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.