Re: [isabelle] Issue with `Simpl` user guide `Fac` example



On Sat, 19 Apr 2014, Lars Noschinski wrote:

You can also add the line

   $AFP

to a file name ROOTS in $ISABELLE_HOME_USER (i.e. ~/.isabelle/ on Unix).

Using a ROOTS file in the proper place is indeed the standard way these
days, although that is little known.

One thing that annoys me a little when I set this, is that I lose the ability to say 'build everything in the distribution' (but not the AFP).

That is the deeper reason why the $AFP entry point is not imposed on users by default, even with initialzed AFP component.

You don't have to include all of $AFP in ROOTS, but just the session root directories you care about (with manually completed dependencies), e.g.

  $AFP_BASE/thys/Simpl

Such entries may be also commented out with # in the ROOTS file, when they are getting in the way at some point.


	Makarius




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