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

[Makarius]

On 10/07/2024 13:23, Makarius wrote:
> 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.

More side-remarks on the local file-system: normally you refer to external 
resources via the "master directory" of the enclosing theory context. 
Isabelle2019 has even introduced an ML antiquotation for that (see NEWS):

* ML antiquotation @{master_dir} refers to the master directory of the
underlying theory, i.e. the directory of the theory file.


For external resources to be editable in the Prover IDE you should use a 
different approach, via Isar commands of the kind "thy_load". Then the system 
takes care of the file content (via the IDE of that is present), and provides 
the text as likes (see Token.file). An example for that is in the HOL-SPARK 
session (Tools/spark_commands.ML etc.)


The next stage of sophistication are external resources generated from 
Isabelle/ML, with 'export_code' as notable application (see NEWS for 
Isabelle2019):

* Commands 'generate_file', 'export_generated_files', and
'compile_generated_files' support a stateless (PIDE-conformant) model
for generated sources and compiled binaries of other languages. The
compilation process is managed in Isabelle/ML, and results exported to
the session database for further use (e.g. with "isabelle export" or
"isabelle build -e").

* Command 'export_code' produces output as logical files within the
theory context, as well as formal session exports that can be
materialized via command-line tools "isabelle export" or "isabelle build
-e" (with 'export_files' in the session ROOT). Isabelle/jEdit also
provides a virtual file-system "isabelle-export:" that can be explored
in the regular file-browser. A 'file_prefix' argument allows to specify
an explicit name prefix for the target file (SML, OCaml, Scala) or
directory (Haskell); the default is "export" with a consecutive number
within each theory.


Thus we are rather far removed from anything like a "local disk" or "local 
file-system". It is about resources that are managed relatively to a theory 
node in the overall session context.


	Makarius