Email Gateway (Mar 22 2021 at 15:40): Email Gateway (Mar 22 2021 at 15:40):From: Alex Meyer <alex153@outlook.lv>
I am working with my own theory file in jEdit and 'Plugins - Isabelle - Browse Session information' shows pretty basic:
So, I assume that HOL is the session name and I am trying to export this session with:
tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle export -O /cygdrive/c/test -x :* HOL
but my current theory file is not in the exported files in C:/test directory.
So - am I exporting the right session? Maybe there is some more specific (child) session under which my custom theory file is being processed and I should export this specific session?
I have made 2 stackoverflow questions about it (with not reaction so far), but it is fine to receive quick answer here. If it solves, then I can transform it into answers to my own SO questions for the reference for others.
My intention is to use the session export for conversion into mmt xml (I have good documentation and source code for that, so I can handle it myself with the current or older versions, I will see).
Alex
Email Gateway (Mar 22 2021 at 15:42):From: Jakub Kądziołka <kuba@kadziolka.net>
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: Jan 04 2025 at 20:18 UTC