Email Gateway (Aug 19 2022 at 08:30): Email Gateway (Aug 19 2022 at 08:30):From: Jens Doll <jd@cococo.de>
Hello all,
I now have a CygWin installation with the Isabelle2012 directory copied
to it's root.
Then I called 'isabelle mkdir MyTheo' and found the directory MyTheo
(somewhere).
Afterwards I created a simple theory myth.thy in that directory and
tried to build it by calling 'isabelle make'.
I got a message of a missing Isamake file.
My two questions are:
a) Why is the makefile needed?
b) Which is the most simple makefile here?
Jens
Email Gateway (Aug 19 2022 at 08:30):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi Jens, and welcome home :)
Just an hypothesis: are you sure you ran the “isabelle make” command from
within the same directory as the one you use to run the “isabelle mkdir”
command?
Say you invoke “isabelle mkdir MySession” from “~/foo”, then it will
create a directory “~/foo/MySession”, will populate it, and will create
the makefile as “~/foo/Isamake”, so you have to run “isabelle make” from
inside of “~/foo”, not from inside of “~/foo/MySession”.
Can you check this prior to anything else?
Email Gateway (Aug 19 2022 at 08:31):From: Jens Doll <jd@cococo.de>
Hello Yannick and all,
thanks for the hint. So I did this
> cd
changed to ~
> /Isa*/bin/isabelle mkdir MyTheo
... that created the directory and some stuff, also the makefile IsaMakefile
... then I created my myth.thy in ../MyTheo and tried to do a make
> /Isa*/bin/isabelle make
Running HOL-MyTheo ...
Unknown logic "HOL" -- no heap file found in:
/cygdrive/c/Users/Jens/.isabelle/Isabelle2012/heaps/polyml-
undefined_x86-cygwin
/Isabelle2012/heaps/polyml-undefined_x86-cygwin
HOL-MyTheo FAILED
What is this about? I thought it had been solved?
Jens
Email Gateway (Aug 19 2022 at 08:31):From: Makarius <makarius@sketis.net>
What do you mean by "the Isabelle2012 directory"? Only the sources?
On the official Isabelle website the front-page has a big green download
button for the fully integrated Isabelle bundle for your platform. If
that does not work (wrong guess of platform) then use one of the smaller
items "Download for Windows" etc.
The self-extracting installer should work out-of-the-box. It might be
something to get used to for someone who has seen older Isabelle
distributions. There is hardly anything left to do by hand.
There are some extra explanations
http://isabelle.in.tum.de/installation.html that are required in rare
situations, such as augmenting the bundled Cygwin by Latex.
Makarius
Email Gateway (Aug 19 2022 at 08:31):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Just to tease, but that may be relevant too: the big download button
doesn't look like a download button, and more looks like an illustrative
picture. A workaround for that ergonomic issue, could be to add all
download links below the picture/button, and to not remove the one
corresponding to the platform which was detected. The download links
hopefully looks like links.
Cheese :-D
Last updated: Nov 21 2024 at 12:39 UTC