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



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.

--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University






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