How to register MMT as Isabelle component on Windows 10 (to call isabelle mmt_build)?

user_1375882 0
Viewed 40

I have installed Isabelle2021 in C:\Homes\Isabelle2021\Isabelle2021 and MMT (from https://uniformal.github.io//doc/setup/) in C:\Homes\MMT21 and I have made additional entries in the C:\Homes\Isabelle2021\Isabelle2021\etc\Components file:

/cygdrive/c/Homes/MMT21
/cygdrive/c/Homes/MMT21/systems/MMT/deploy

But my cygwin-terminal.bat command gives the error that the component can not be found:

C:\Homes\Isabelle2021\Isabelle2021>cygwin-terminal
This is the GNU Bash interpreter of Cygwin.
Use command "isabelle" to invoke Isabelle tools.

tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle mmt_build
*** Unknown Isabelle tool: "mmt_build"

tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021

I have tried to follow https://drops.dagstuhl.de/opus/volltexte/2020/13065/pdf/LIPIcs-TYPES-2019-1.pdf:

if the Mmt directory is registered to Isabelle as component, it provides a tool isabelle mmt_build (shell script) to build MMT with Isabelle support enabled. The resulting mmt.jar will provide further tools isabelle mmt_import and isabelle mmt_server (in Scala) to perform the import and view its results. Users merely need to invoke, e.g., isabelle mmt_import -B ZF.

What is wrong with my efforts? Does the registration of Isabelle component required additional activies? And is mmt.jar really so adapted to Isabelle (one specific tool in opposition of MMT being the very universal system) that mmt.jar really contains such mmt_build command?

I am going to read https://isabelle.in.tum.de/dist/Isabelle2021/doc/system.pdf Chapter 7.2 "Managing Isabelle Components", maybe it will help and maybe it will work on Windows...

isabelle mmt
1 Answers

This is partial answer. Simple addition of the MMT directory was not possible due to error messages:

tomr@ /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle components -x /cygdrive/c/Homes/MMT21
*** Bad component directory: "/cygdrive/c/Homes/MMT21"

I found in the Isabelle source code https://isabelle-dev.sketis.net/file/data/ldiwqhsxa4d5zojczqye/PHID-FILE-2yuwbxlojqunqpdcqvqg/file the reason for this:

def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit =
   {
     val path = path0.expand.absolute
     if (!(path + Path.explode("etc/settings")).is_file &&
         !(path + Path.explode("etc/components")).is_file) error("Bad component directory: " + path)

So, it is required (for directory to be used as the Isabelle component) that MMT directory contains etc/settings file. MMT didn't have one, so, I grabbed one such file from the existinc Isabelle components and I modified it to be:

# -*- shell-script -*- :mode=shellscript:

classpath "C:/Homes/MMT21/mmt.jar"

isabelle_scala_service "isabelle.FlatLightLaf"
isabelle_scala_service "isabelle.FlatDarkLaf"

After having that file in MMT21 directory I managed to add MMT21 as a component:

tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle components -u /cygdrive/c/Homes/MMT21
Added component "/cygdrive/c/Homes/MMT21"

But, unfortunately, it didn't solve my initial problem, I am still getting an error:

tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle mmt_build
*** Unknown Isabelle tool: "mmt_build"

So, know I am going deep down into Google and into respective project sites to dig this out...

ADDED: There are good materials https://sketis.net/2019/mmt-as-component-for-isabelle2019 and https://github.com/UniFormal/MMT/tree/master/src/mmt-isabelle about this, so, it appears, that there is special jar, not the main mmt.jar. I am now reading about this. I will see whether it this works with Isabelle2021 or should I use it with my older Isabelle2020.

user_13758820
Related