Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Is there an “isabelle make” tutorial?

view this post on Zulip Email Gateway (Aug 19 2022 at 08:33):

From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi all once again,

I feel so poor and miserable at understanding how “isabelle make” works, I
believe I should seek for a tutorial about Isabelle variant of make. I've
read “~~/doc/system.pdf” multiple times, but I'm still failing to figure
what's wrong.

Example of what's going wrong:

* When I've updated the theory file and run “isabelle make”, it says
“nothing to do”

* Consequence of the above, I have to always invoke “isabelle make clean”
prior to “isabelle make TARGET”

* BASE_DEPENDENCIES seems to be ignored
* Produced PDF files always go in an hidden directory beneath
$HOME/.isabelle

* Seems “-V document=theory,proof,ML” specified for USEDIR is ignored in
IsaMakefile and always produce both “document.pdf” and “outline.pdf”

* Specifying the “-b” option for USEDIR, it always complains ROOT.ML is
missing
(an SML program ends with an I/O error exception)

* and so on

I'm able to run the basic “isabelle mkdir MySession; isabelle make” with
an updated ROOT.ML, fine, but any attempt to go beyond that, fails.

view this post on Zulip Email Gateway (Aug 19 2022 at 08:33):

From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Le Tue, 07 Aug 2012 22:48:48 +0200, Makarius
<makarius@sketis.net> a écrit:

On Tue, 7 Aug 2012, Yannick Duchêne (Hibou57) wrote:

I feel so poor and miserable at understanding how “isabelle make” works,
I believe I should seek for a tutorial about Isabelle variant of make.
I've read “~~/doc/system.pdf” multiple times, but I'm still failing to
figure what's wrong.

Basically the chaper 3 of system.pdf is the tutorial. Isabelle make is
in
fact easy to explain 100% in 1 line, by giving its implementation:

exec make -f IsaMakefile "$@"

The rest of the complexity is in "make" and "IsaMakefile". There are
many
versions of "make", and all of them are very complex. The IsaMakefile
can
in principle do whatever it pleases with the available tools, notably
"isabelle usedir" and "isabelle document", but one should imitate
existing
examples closely.

BTW, this is the last release with the canon of isabelle mkdir / usedir /
make / makeall tools -- I am working on the replacement since a couple of
weeks already, after more than 15 years of suffering from isabelle make
myself.

OK, I will wait that couple of weeks and learn about the new design (P.S.
Me too, I don't enjoy the *NIX make command)

Example of what's going wrong:

This indicates that your dependencies are not properly declare. The bad
thing about "make" is that you have to do it yourself, but variants of
GNU
make allow approxitive .thy document/.tex for example.

What are BASE_DEPENDENCIES?

Somewhere, in a ~~/doc/*.pdf documents, there was a sentence directing to
~~/src/HOL/IsaMakefile. I saw this definition, and as I had troubles with
dependencies, I though the answer was this. So I was wrong, OK.

You can say "usedir -d false -D generated" to dump the sources in
"generated/" relatively to the session sources, and then run "isabelle
document" on the result.

So I have to generate the PDF documents separately, OK.

Did you actually pass it to the usedir invocation, not just define a
USEDIR variable in the IsaMakefile?

I did it with the USEDIR variable, as though it was the most recommanded
way.

Better avoid the -b option; for historic reasons it assumes a quite
different directory layout: everything in "." instead of the session
directory.

I see. I was misleaded by the Example vs Build and though Example was not
intended for regular use.

The problems of "make" are indeed endless. In the next release, it will
no longer be used for Isabelle.

I'm able to run the basic “isabelle mkdir MySession; isabelle make”
with an
updated ROOT.ML, fine, but any attempt to go beyond that, fails.

Try staying closer to the generated IsaMakefile. Uncomment the -D
generated option. Add some .thy document/.tex dependencies.

Makarius

Will do that (using the proper Makefile way I guess), thanks for you
valuable comments.

view this post on Zulip Email Gateway (Aug 19 2022 at 08:33):

From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
After Markus's comments,

Attached document, is an IsaMakefile template. Tested with GNU make (may
not work with other make variant). It's simple enough, you just have to
change “Isa_Test” to match your session name. It rebuilds the session
whenever a theory file has changed, builds “document.pdf”, and IsaMakefile
has a dependence to it‑self, so that build is considered dirty if ever you
change any thing in IsaMakefile.

As usual, don't forget too, to setup your ROOT.ML file properly.
IsaMakefile

view this post on Zulip Email Gateway (Aug 19 2022 at 08:33):

From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Sorry, please read “Makarius's comments” (was not the sole time I did this
error)

Last updated: Apr 19 2024 at 04:17 UTC