Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Pārs.: How to see the names of all active Is...


view this post on Zulip Email Gateway (Mar 27 2021 at 14:41):

From: Alex Meyer <alex153@outlook.lv>
OK, I have solved my problem. Indeed - it is required to add every new theory file to the ROOT manually. Actually - one should work at lot with the ROOT file and keep it updated manually all the time - this is my conclusion which has not beend stressed enough in the guides and tutorials on Isabelle.

So - I have added my theory file to C:\Workspace-Algo\Max_Of_Two_Integers_Real.thy and my ROOT is now:

session Algo = HOL +
options [document = pdf, document_output = "output"]
(*theories [document = false]
A
B
theories
C
D*)
theories
Max_Of_Two_Integers_Real
document_files
"root.tex"

The export proceeded normally:

tomr@DESKTOP /cygdrive/c/Workspace-Algo
$ isabelle export -d /cygdrive/c/Workspace-Algo -O /cygdrive/c/test3 -x :* Algo
Build started for Isabelle/Algo ...
Running Algo ...
Preparing Algo/document ...
Finished Algo/document (0:00:11 elapsed time)
Document at "/cygdrive/c/Workspace-Algo/output/document.pdf"
Finished Algo (0:00:02 elapsed time)
export "/cygdrive/c/test3/Algo.Max_Of_Two_Integers_Real/PIDE/document_id"
export "/cygdrive/c/test3/Algo.Max_Of_Two_Integers_Real/PIDE/files"
export "/cygdrive/c/test3/Algo.Max_Of_Two_Integers_Real/PIDE/markup"
export "/cygdrive/c/test3/Algo.Max_Of_Two_Integers_Real/document/Max_Of_Two_Integers_Real.tex"

I had to correct my thy file, export command checked and reported errors, but after correcting them the export proceeds normally and there is both: 1) output directory with tex and PDF files and 2) isabelle export -O C:/test3 output dump which contains the most important file C:\test3\Algo.Max_Of_Two_Integers_Real\PIDE\markup with cryptic content:

keyword1kind=commandentityref=28088def_line=76def_offset=2697...

Now, I guess, I will be able to forward this to Isabelle/MMT for translation into MMT/XML.

So - this step is solved and I can more forward. Thanks!

Alex


No: Alex Meyer <alex153@outlook.lv>
Nosūtīts: sestdiena, 2021. gada 27. marts 17:21
Kam: Jakub Kądziołka <kuba@kadziolka.net>; Isabelle Users <isabelle-users@cl.cam.ac.uk>
Tēma: Atb.: [isabelle] How to see the names of all active Isabelle sessions and how to export specific session?

Dear friends, I am really stuck with this, hope, someone can help moe to overcome this and move forward. So this is what I am doing step-by-step:

I crated session root in directory Workspace-Algo with session name Algo:

tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ cd /cygdrive/c/Workspace-Algo

tomr@DESKTOP /cygdrive/c/Workspace-Algo
$ isabelle mkroot -n Algo

Preparing session "Algo" in "."
creating "ROOT"
creating "document/root.tex"

Now use the following command line to build the session:

isabelle build -D .

My ROOT file is:

session Algo = HOL +
options [document = pdf, document_output = "output"]
(*theories [document = false]
A
B
theories
C
D*)
document_files
"root.tex"

I have copied my theory file Max_Of_Two_Integers_Real.thy inside document subdirectory:

theory Max_Of_Two_Integers_Real
imports (* Main *)
(* "HOL.Imperative_HOL‹›
Subarray *)
"HOL-Library.Multiset"
"HOL-Library.Code_Target_Numeral"
"HOL-Library.Code_Target_Nat"
"HOL-Library.Code_Abstract_Nat"
begin

definition two_integer_max_case_def :: "nat ⇒ nat ⇒ nat" where
"two_integer_max_case_def a b = (case a > b of True ⇒ a | False ⇒ b)"

definition "example_case_def = two_integer_max_case_def 1 2"

(*
export_code example_case_def checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
*)

(* test 123 *)

end

I built session and started jEdit from command line from the session directory:

tomr@DESKTOP /cygdrive/c/Workspace-Algo
$ isabelle build
0:00:02 elapsed time

tomr@DESKTOP /cygdrive/c/Workspace-Algo
$ isabelle jedit -d /cygdrive/c/Workspace-Algo

'Plugins - Isabelle - Browse Session information' shows session structure:
isabelle-session:
Unsorted
file Unsorted/Algo
That is fine, one can say that I am in my session indeed.

But the default file is scratch and I should open my thy file manually. Let it be.

And now is the main thing.

I tried to export my Algo session:

tomr@DESKTOP /cygdrive/c/Workspace-Algo
$ isabelle export -d /cygdrive/c/Workspace-Algo -O /cygdrive/c/test3 -x :* Algo
Build started for Isabelle/Algo ...
Running Algo ...
Preparing Algo/document ...
Finished Algo/document (0:00:21 elapsed time)
Document at "/cygdrive/c/Workspace-Algo/output/document.pdf"
Finished Algo (0:00:01 elapsed time)

This export created /Workspace-Algo/output directory with tex and tex style files and session graph pdf and so on. But what I was really after and and what I have tried to achieve was export to C:/test3 directory in which I expected to see theory and proof files - files without extension that are some kind of session internal dump files which I can forward to MMT tool for transformation into XML MMT files according to https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2021-March/msg00069.html

So - I have 2 problems here and I am looking for 2 answers:

1) Why my Max_Of_Two_Integers_Real.thy has not been included in output directory and why session graph.pdf is empty? I expect: if I am starting jEdit from the session directory and I am starting theory file from such jEdit instance, then I expect that theory file is automatically being added to the sessions. Or is it no? Should I add every theory file manually to the session ROOT file? And only then the session build transmits this theory file to output?

2) Why my export technical dump (not to confuse it with the tex/pdf output in output directory) to C:/test3 is empty - no sessions, no proofs, no heaps etc.? Is it because my session ROOT does not contain explicitly listed theory files? If I had added theory files manually to ROOT file, then session would have had some content and this technical content would have beend exported to isabelle export -O directory?

Hope, that someone can clarify those things for me.

I have gone through hard things before. And I know how to cope with them - I have gone through quantum mechanics or Yoned lemma in category theory and the rule of thumb is to go after second, third... sixth, seventh book and have wide outlook on the things and such persistence clear away all the confusions and leads to understanding. But for Isabelle there are not sixth or seventh tutorial or manual. So, that is why I am asking here. Thanks in advance!

Alex


No: Jakub Kądziołka <kuba@kadziolka.net>
Nosūtīts: pirmdiena, 2021. gada 22. marts 17:41
Kam: Alex Meyer <alex153@outlook.lv>; Isabelle Users <isabelle-users@cl.cam.ac.uk>
Tēma: Re: [isabelle] How to see the names of all active Isabelle sessions and how to export specific session?

You need to create a session with 'isabelle mkroot', just like you would
for document preparation. Then, include the -d flag to point to the
directory in which your ROOT file resides.

Regards,
Jakub Kądziołka


Last updated: Jul 15 2022 at 23:21 UTC