Email Gateway (Mar 28 2021 at 01:27): Email Gateway (Mar 28 2021 at 01:27):From: Alex Meyer <alex153@outlook.lv>
I have theory with 2 definitions and some 20 LOC including the usual boilerplate.
I have completed mmt_import with Isabelle_MMT-20190611.exe from https://sketis.net/2019/mmt-as-component-for-isabelle2019 . I used command:
tomr@DESKTOP /cygdrive/c/Homes/Isabelle_MMT-20190611/Isabelle_MMT-20190611
$ isabelle mmt_import -D /cygdrive/c/Workspace-Algo
Adding archive C:\Homes\Isabelle_MMT-20190611\Isabelle_MMT-20190611\isabelle_test
Loading 3 sessions ...
Processing theory Pure ...
Starting session Pure ...
Loading 112 theories ...
Processing theory HOL.Code_Generator ...
...
...
/cygdrive/c/Workspace-Algo is my theory session directory (with ROOT in it) and C:\Homes\Isabelle_MMT-20190611\Isabelle_MMT-20190611\isabelle_test is some test directory inside Isabelle-MMT-2019 combined installation, I don't know why mmt_import requires/works on it. For the sake of security I copied all the content from my theory session directory /cygdrive/c/Workspace-Algo to this C:\Homes\Isabelle_MMT-20190611\Isabelle_MMT-20190611\isabelle_test as well.
All in all - mmt_import exported more than 100 theories and it took 45 minutes on Intel7/16GB RAM machine with almost total consumption of all awailable RAM.
So, the questions:
* Is there a way to indicate that I would like to export only 1 theory and not the remaining theories which somehow (indirectly) can be required for export?
* Is there a way to ask not to export the base theories once more: e.g. indicate that base theories have already been exported and to provide path to exports and then the proper export of the propert single theory could be fast?
* Why RAM consumption, consumption of resources ir so large?
* Is it hard to upgrade mmt_import 2019 for Isabelle2021. What it takes? Maybe I can do it myself, but some quick guidance could be good?
* I guess - if I would like to improve mmt_import or dig deeper, then I should be very good at Isabelle/Scala implementation. I checked System manual and there is Chapter 5 about Isabelle/Scala systems programming - as I understand, that is all for Isabelle/Scala?
* As I understand - if I would like to form my own Isabelle textual commans and send programmatically them to Isabelle and recieve response etc. then I should use Isabelle/Scala interface, am I right on this point? There is nothing more appropriate? (We have already discussed this about theory export in JSON/XML and as I understood - then every export tool, every interaction tools boils down to Isabelle/Scala - so - it should be worth to lear it).
And lastly - just quick question: I installed mmt-20190611.tar.gz (un-gzipped, un-tarred and installed) as components for Isabelle2021 and I tried to run - I got errors about isabelle_scala_tools:
tomr@DESKTOP /cygdrive/c/Workspace-Algo
$ isabelle components -u /cygdrive/c/Homes/IsabelleMMT/mmt-20190611
Added component "/cygdrive/c/Homes/IsabelleMMT/mmt-20190611"
tomr@DESKTOP /cygdrive/c/Workspace-Algo
$ isabelle mmt_import
/cygdrive/c/Homes/IsabelleMMT/mmt-20190611/MMT-17.0.0/src/mmt-isabelle/etc/settings: line 11: isabelle_scala_tools: command not found
Return code 127 from bash script: "/cygdrive/c/Homes/IsabelleMMT/mmt-20190611/MMT-17.0.0/src/mmt-isabelle/etc/settings"
Well, I know that this is bad thing to do - documentation explicitly required total compatibility of releases between Isabelle-MMT and Isabelle and in this case I am violating it by 2 major version, but still - what could it take to upgrade mmt_import for Isabelle2021? Maybe I can somehow installa isabelle_scala_tools and all the remaining will work anyway?
Well - and just one last question. I am trying to do externa manipulation (parsing, machine learning and generating) Isabelle code and see, how hard is this. Maybe someone have experience with Coq and Lean with the similar tasks - parsing, machine learning and generating? Maybe it is easier and why easier? Isabelle's large and ever growing AFP is the strongest case why I am so fond of Isabelle, but still...
Thanks in advance!
Alex
Email Gateway (Mar 28 2021 at 13:35):From: Makarius <makarius@sketis.net>
On 28/03/2021 03:26, Alex Meyer wrote:
I have completed mmt_import with Isabelle_MMT-20190611.exe from
https://sketis.net/2019/mmt-as-component-for-isabelle2019
That is a rather old blog entry on an ongoing project; it was later released
with Isabelle2020 and published in
https://drops.dagstuhl.de/opus/volltexte/2020/13065
For Isabelle2021, I have updated the mmt-isabelle sources here:
https://github.com/UniFormal/MMT/commit/43fec2b39fba --- that is not a proper
release of MMT, but that project is somewhat experimental anyway.
If you do want to continue with MMT, you should:
* use its Scala libraries to access the XML/OMDoc content, not your own
homegrown tools for this complex format;
* get acquainted with how MMT is built and run: it should be fine on
Windows, because its main developer Florian Rabe is also on that platform;
* get in touch with the MMT community and ask further questions over there.
MMT might even help you to get both Isabelle and Coq on board of your project,
but it is not "for free": it requires to work with the structures of MMT
systematically, notable the LF (Logical Framework) meta-theory.
An alternative is to harvest HTML presentations of Isabelle, Coq etc. Since AI
is inaccurate anyway, that could make sense: you get sources that are
annotation with the role of identifiers etc. (colors, maybe also links).
In Isabelle2021, the standard HTML output merely produces colors, but you can
use a little bit of Isabelle/Scala to access the Markup.ENTITY elements as
well. Here is the entry point for "isabelle build -P:"
https://isabelle.sketis.net/repos/isabelle-release/file/Isabelle2021/src/Pure/Tools/build.scala#l494
(the build tool is described in the "system" manual).
By using "isabelle scala_project" with Gradle and IntelliJ IDEA as described
in the same text, you can easily explore the specification written as Scala
source text. (MMT is more complex and irregular, but I still managed rather
quickly to understand its main points with the help of IntelliJ IDEA.)
All in all - mmt_import exported more than 100 theories and it took 45 minutes
on Intel7/16GB RAM machine with almost total consumption of all awailable RAM.
16GB is not much for full-scale Isabelle applications. Isabelle/MMT from 2019
requires more than that, although in 2020 I improved that a lot.
In 2021, I've built PIDE markup into regular "isabelle build" + "isabelle
export", so the bulky "isabelle dump" (or Headless session in Isabelle/MMT) is
no longer required. Isabelle/MMT will eventually be updated in that respect,
but I can't say when.
* Is there a way to indicate that I would like to export only 1 theory and
not the remaining theories which somehow (indirectly) can be required for
export?
* Is there a way to ask not to export the base theories once more: e.g.
indicate that base theories have already been exported and to provide path
to exports and then the proper export of the propert single theory could
be fast?
* Why RAM consumption, consumption of resources ir so large?
* Is it hard to upgrade mmt_import 2019 for Isabelle2021. What it takes?
Maybe I can do it myself, but some quick guidance could be good?
* I guess - if I would like to improve mmt_import or dig deeper, then I
should be very good at Isabelle/Scala implementation.
These questions are only of historic interest. The proper answer is to ask
different questions: How use Isabelle2021 with Isabelle/Scala properly?
The "system" manual refers to "isabelle scala_project" + Gradle + IntellJ
IDEA: you should purchase 16 GB more RAM and use that.
* As I understand - if I would like to form my own Isabelle textual commans
and send programmatically them to Isabelle and recieve response etc. then
I should use Isabelle/Scala interface, am I right on this point? There is
nothing more appropriate? (We have already discussed this about theory
export in JSON/XML and as I understood - then every export tool, every
interaction tools boils down to Isabelle/Scala - so - it should be worth
to lear it).
Isabelle commands are defined in Isabelle/ML. Regular Isabelle/jEdit is the
main IDE for that: just look a bit through the "implementation" manual or
better the sources: $ISABELLE_HOME/src/Doc/Implementation/Integration.thy it
has a reference e.g. to
$ISABELLE_HOME/src/HOL/Examples/Commands.thy
Well, I know that this is bad thing to do - documentation explicitly required
total compatibility of releases between Isabelle-MMT and Isabelle and in this
case I am violating it by 2 major version, but still - what could it take to
upgrade mmt_import for Isabelle2021?
Doing bad things is no good. The proper way is to use the already updated
Isabelle/MMT (see above), if you want to use it at all.
Well - and just one last question. I am trying to do externa manipulation
(parsing, machine learning and generating) Isabelle code and see, how hard is
this. Maybe someone have experience with Coq and Lean with the similar tasks -
parsing, machine learning and generating? Maybe it is easier and why easier?
Isabelle's large and ever growing AFP is the strongest case why I am so fond
of Isabelle, but still...
Isbelle/AFP is indeed the greatest success of the prover community as a whole.
No other proof assistant has gone as far yet, concerning both the technology
and the content.
If you want to harvest just that, I would recommend a regular "isabelle build
-d AFP/thys -a" with some Isabelle/Scala tool to process the PIDE markup
(accessing not the raw YXML data, but using typed functions).
To work with all of AFP, you should have 32-64 GB RAM, and as many CPU cores
as you can get.
Makarius
Last updated: Apr 18 2024 at 04:17 UTC