Re: [isabelle] newbie questions r.e. Isar to Haskell/ML generation



On Fri, 7 Dec 2012, Aaron Gray wrote:

Thank you for the information and a path forwards. I will try running Linux in a VM tomorrow. I have Linux servers but they are headless. And I have Windows/Cygwin/Java 1.7 problems using the development branch.

Since "the" development branch is continously moving, you should subscribe to the isabelle-dev mailing list and post any observations and problems there. We are aready moving towards the next stable release, and I have recently started to make it again easier to get it running on Windows.

It would be interesting to know what were your problems with Java 7, because that will be very important for the coming Isabelle release. (Did you try to download add-components yourself? You shouldn't. See the explanations in README_REPOSITORY in the toplevel directory of the Mercurial clone.)

Follow-ups on isabelle-dev, where anything related to arbitrary Isabelle repository versions belongs. You should also have changeset ids ready, when pointing to the version that you have.


Then will look into using Java native on Windows with MinGW for Bash rather than via Cygwin. It would also be nice to have an environment that is not dependent upon Bash though.

Isabelle depends on much more than just bash, and I don't understand why it should be avoided. Cygwin is also essential for many add-on tools and Poly/ML as well. It is not realistic to change such system integration things as a "newbie" as you've called yourself. Even for myself after so many years of Isabelle integration and distribution management it is always a struggle to get things forward and work more smoothly for more users.


Has/is Isabelle/HOL been/being migrated to Scala from ML ? If so do you know what the status is here ?

Isabelle has many languages and many aspects. ML remains the main implementation and extension language for the logical parts. Scala is already the main system programming language, including front-end tools etc. (Doing POSIX-oid things on Scala/JVM is quite odd to implement, but it works out in the end.)

There are also connections between the different Isabelle languages. For example, you can use

  ML {* val a = 1 *}

inside the Isar source language of .thy files routinely for many years.

Moreover you can invoke Isabelle/Scala from there like this:

  ML {* Invoke_Scala.method "java.lang.System.getProperty" "user.home" *}

That gives you a String => String interface between the ML and Scala world, and you can then use Isabelle XML/YXML data encoding to transport actual content easily.

Note that Invoke_Scala.method currently only works while Isabelle/jEdit is running. Wrapping the Isabelle/Scala process around any Isabelle session is still open, and won't happen for the coming release.


	Makarius






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