Re: [isabelle] The instructions in AFP's "Using Entries" do not work



On 25/05/2021 23:36, Jakub Kądziołka wrote:
> Hello,
> 
> at the Isabelle Zulip, we have just successfully troubleshot an issue
> with getting Isabelle to recognize AFP component. As it turns out, the
> path that should be included in $ISABELLE_HOME_USER/etc/components
> (which is, by the way, incorrectly referred to by `isabelle components --help`
> as $ISABELLE_HOME_USER/components, without the /etc/ path component),
> is .../afp-2021-05-14/thys, and not just .../afp-2021-05-14.
> Moreover, `isabelle components -u` will only accept the former,
> rejecting the latter with
> 
> *** Bad component directory: "/home/kuba/formal/afp-2021-05-14/thys"
> 
> Manually editing $ISABELLE_HOME_USER/etc/components to include the path
> to .../thys makes things work.

As a "proof" for the formal record, here is the public archive of the Zulip
thread in question:
https://isabelle.systems/zulip-archive/238552BeginnerQuestions/77272afp.html

Already in 1990, I have resolved to ignore the real-time chat culture, so it
is indeed important to copy topics that might be relevant over to the official
mailing list.


First some minor notes, especially on the idealized situation for the next
release:

* The official way to get usage help for Isabelle tools is via the non-option
"-?": the isabelle executable says that.

* I have already updated the usage message here:
https://isabelle.sketis.net/repos/isabelle/rev/f73c691bd679

* "isabelle components -u" is indeed a bit rough in Isabelle2021: I introduced
it for something marginal elsewhere, before it got more attention in the last
moment in simplifying AFP setup.

* The check for etc/settings or etc/components is actually too strict: both
are optional and a meaningful component directory can have just ROOT and/or
ROOTS as we see in AFP/thys. See also
https://isabelle.sketis.net/repos/isabelle/rev/c8b4a4f69068


I will answer Gerwin's answer separately, especially for Isabelle2021 without
any of these changes.


	Makarius




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