[isabelle-dev] Duplicate theory??

Makarius makarius at sketis.net
Tue Apr 9 12:11:59 CEST 2019


On 09/04/2019 12:09, Lawrence Paulson wrote:
> Thanks. What about a single entry?
> 
> isabelle build -d '$AFP' Groebner_Bases
> *** Undefined Isabelle environment variable: "AFP"
> 
>> On 9 Apr 2019, at 10:59, Makarius <makarius at sketis.net> wrote:
>>
>>  # almost all of Isabelle + AFP together
>>  isabelle build -d '$AFP' -a -X very_slow
>>
>>  # only AFP + its requirements
>>  isabelle build -D '$AFP'

You still need a proper "init_components" for AFP, in order to see the
$AFP variable.

Of course, you should be able to omit that and refer to the AFP/thys
directory directly, wherever that is. (I use this scenario often after a
rsync of Isabelle + AFP to some fast test machine, e.g. lxcisa0.)


	Makarius




More information about the isabelle-dev mailing list