Email Gateway (Aug 19 2022 at 09:28): Email Gateway (Aug 19 2022 at 09:28):From: Aaron Gray <aaronngray.lists@gmail.com>
Hi,
I am new to Isabelle/HOL and Isar in general although I know the principles
and am familiar with languages like Z. And with Haskell and ML.
I am trying to work out how to use the jEdit IDE, but would prefer to work
from command line as well.
How do I generate Haskell and ML and friends from a proof like CoreC++ for
example ?
Many thanks in advance,
Aaron
Email Gateway (Aug 19 2022 at 09:28):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Aaron,
How do I generate Haskell and ML and friends from a proof like CoreC++ for
example ?
As far as I know, you cannot generate Haskell code from a "proof", but just from
definitions and functions, and in certain cases also from inductive definitions
by using the predicate compiler.
In principle, everything that can be written as an equality "lhs = rhs" can be fed
to the code-generator.
lemma [code]: "lhs = rhs"
proof ...
declare my_theorem[code]
then getting the code is as easy as writing
export_code some_function in Haskell file ...
however, it might fail whenever there are non-executable involved.
For example, defining
definition fermat where "fermat n = (?x y z. x > 0 /\ y > 0 /\ x^n + y^n = z^n)"
then
export_code fermat in Haskell file -
will fail, but if you first prove a code-equation
lemma fermat_code[code]: "fermat n = (n <= 2)"
proof ...
then of course it will become executable.
Further information on the code-generator can be found by
isabelle doc codegen
Hope this helps,
René
Email Gateway (Aug 19 2022 at 09:28):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear Aaron,
it is not clear to me what you mean by generating code from a proof like
CoreC++. A proof of a theorem is not executable in ML or Haskell, only Isabelle
can check the proof. However, you can generate ML and Haskell code from
definitions in a formalisation, if they satisfy the restrictions of Isabelle's
code generator. The generated code then executes the definitions, not the
proofs. By the correctness of the code generator (unless someone messed with the
setup), the output of the generated code then is correct in the sense that you
could prove in Isabelle that the result is the denotation of the definitions for
the given input.
For CoreC++ in particular, the big-step semantics and the type system are
executable. This means that you can run CoreC++ programs in the semantics and
that you can infer the type of a statement or expression. Only two weeks ago, I
have spent a few days on reactivating the setup which got broken due to changes
in Isabelle's code generator. So, if you want to execute CoreC++, you need to
use the development version of the AFP. Most probably, this version will not
work with Isabelle2012, so you also have to use the development version, e.g.,
from http://isabelle.in.tum.de/devel/.
Now, back to your question. The export_code keyword generates such code. For
CoreC++, you might put these five lines into a file in the same folder as
CoreC++ and load it in jedit:
theory Code_Generation imports Execute begin
export_code big_step WT WT_i_i_i_o
in SML module_name CoreCpp
file "path_to_my_file.ML"
end
Once this file is processed, the code for the big step semantics, type checks
and type inference is in the file, along with the abstract syntax definition for
the CoreC++ language.
You can export to other language by replacing the "in SML ..." line as needed,
see the code generator tutorial for that.
If you prefer the command line, there's also Isabelle codegen tool with hardly
any documentation.
Once you have managed to get so far, you are now ready to execute CoreC++
programs. However, the type system and semantics expect the input to be in
CoreC++ abstract syntax, so you cannot feed in C++ programs directly. Daniel
Wasserrab once had a converter from C to CoreC++, but this has never been
adapted to the changes in Isabelle's code generator. So it probably won't work
out of the box. It should still work with the old generated ML files which
Daniel probably has somewhere, so you might ask him.
If you just want to try one small program in CoreC++, the easiest way is to
follow the examples in Execute.thy: Manually convert the program into CoreC++
syntax and define it inside Isabelle as a constant. Then, you can use the values
command to execute it.
Hope this helps,
Andreas
Email Gateway (Aug 19 2022 at 09:28):From: Aaron Gray <aaronngray.lists@gmail.com>
Dear Andreas,
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.
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.
Has/is Isabelle/HOL been/being migrated to Scala from ML ? If so do you
know what the status is here ?
Regards,
Aaron
Email Gateway (Aug 19 2022 at 09:29):From: Aaron Gray <aaronngray.lists@gmail.com>
Dear René,
Thanks for the info and tips. Hopefully I will get somewhere tomorrow.
Regards,
Aaron
Email Gateway (Aug 19 2022 at 09:29):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 09:40):From: andreas.lochbihler@kit.edu
Dear Aaron,
Sorry for the late response, I have been out of office for 3 weeks.
This looks like you are using the Isabelle2012 version of CoreC++ from
http://afp.sourceforge.net/entries/CoreC++.shtml and not the
development version of the AFP from
http://afp.sourceforge.net/devel-entries/CoreC++.shtml. The above code
works fine for me with the latter.
Hope this helps,
Andreas
Last updated: Nov 21 2024 at 12:39 UTC