[isabelle-dev] download-components

Makarius makarius at sketis.net
Wed Aug 8 11:10:41 CEST 2012


On Wed, 8 Aug 2012, Christian Sternagel wrote:

> Dear Florian,
>
> the script you introduced in
>
>  http://isabelle.in.tum.de/repos/isabelle/rev/c895e334162c
>
> is rather useful. How about also providing a variable (as TMP for the 
> download directory) to set the actual isabelle tool (with default "isabelle") 
> instead of hard-wiring "isabelle" (which does not work all too well, when 
> having different isabelle versions installed)?

It is high time to make the Admin directory an Isabelle component, see 
0bc8d90d2717, and to gradually raise the quality standards of the scripts 
there towards that of the Isabelle distribution in general.

I've already added "isabelle update_keywords" in 0bc8d90d2717, although it 
still lacks a proper "usage" for illegal command line, even just the 
conventional '-?' as error that leads to usage display.)

Note that I've now used the "_" to separate words in conformance to other 
Isabelle tools, like tptp_sledgehammer.  This is also more portable, 
because the "-" cannot be passed through nested /bin/sh as shell function 
(which is the reason why isabelle-process still has some snags in exotic 
situations).


 	Makarius




More information about the isabelle-dev mailing list