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



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.


Example of what's going wrong:

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

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.


* BASE_DEPENDENCIES seems to be ignored

What are BASE_DEPENDENCIES?


* Produced PDF files always go in an hidden directory beneath $HOME/.isabelle

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.


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

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


* Specifying the “-b” option for USEDIR, it always complains ROOT.ML is missing

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


* and so on

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


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