Re: [isabelle] The instructions in AFP's "Using Entries" do not work
- To: Jakub Kądziołka <kuba at kadziolka.net>, isabelle-users at cl.cam.ac.uk
- Subject: Re: [isabelle] The instructions in AFP's "Using Entries" do not work
- From: Makarius <makarius at sketis.net>
- Date: Sat, 5 Jun 2021 21:17:49 +0200
- Authentication-results: cam.ac.uk; iprev=pass (mta0.cl.cam.ac.uk) smtp.remote-ip=184.108.40.206; spf=softfail smtp.mailfrom=sketis.net; dkim=pass header.d=sketis.net header.s=key2 header.a=rsa-sha256; arc=none
- Authentication-results: cam.ac.uk; iprev=pass (relay.yourmailgateway.de) smtp.remote-ip=220.127.116.11; spf=pass smtp.mailfrom=sketis.net; dkim=pass header.d=sketis.net header.s=key2 header.a=rsa-sha256; arc=none
- Authentication-results: mx2f26; spf=pass (sender IP is 18.104.22.168) smtp.mailfrom=makarius at sketis.net smtp.helo=[192.168.179.20]
- In-reply-to: <CBMNEY3EWBQ1.1PUX2UDUHJ384@gravity>
- References: <CBMNEY3EWBQ1.1PUX2UDUHJ384@gravity>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.8.1
On 25/05/2021 23:36, Jakub Kądziołka wrote:
> 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:
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
First some minor notes, especially on the idealized situation for the next
* 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:
* "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
I will answer Gerwin's answer separately, especially for Isabelle2021 without
any of these changes.
This archive was generated by a fusion of
Pipermail (Mailman edition) and