[isabelle-dev] Announcing the Isabelle Build Manager: https://build.proof.cit.tum.de

[Makarius]

 > On 7/9/24 17:00, Lawrence Paulson wrote:
 >
 >> I wonder if you could be a bit more explicit about how to use the new system
 >> for testing the distribution and AFP. The commands we use locally often
 >> refer to pathnames on one's local disc, which clearly cannot work here.

On 10/07/2024 09:21, Fabian Huch wrote:
> Paths in Isabelle/AFP are resolved symbolically, and thanks to Makarius' 
> efforts, the build tool can work with them even if absolute paths are different.
> 
> Where do you refer to pathnames? For selecting sessions? You'll have to 
> specify their names instead -- the build_task tool does not have the -d/-D 
> options, and working with paths that have no formal status within Isabelle/AFP 
> is currently not supported. Though this would in principle also be possible.

The current situation (e.g. Isabelle/e066cc867115) is indeed that only the 
Isabelle distribution and AFP are supported (usually via option -A). Then all 
sources ("project directories") will be accessible via 
$ISABELLE_HOME/dirs/ROOT in the target space, after synchronization.


At a later stage, I will add support for arbitrary -d or -D options, to 
include more material to $ISABELLE_HOME/dirs in the target. (It require some 
remapping of given directories relatively to their respective "roots", e.g. 
the top directory of the underlying repository.)

Right now, you can imitate that behaviour by adding add-hoc entries e.g. 
$ISABELLE_HOME/src/HOL/ROOT with a directory in that vicinity (and of course 
push anything).


Side-remark concerning "local disc": Hardly anybody has an actual disk 
anymore, it is just a bad habit to continue using that expression. And 
conceptually, you really mean the "local file-system", so why not say that?


	Makarius