Email Gateway (Mar 01 2021 at 08:11): Email Gateway (Mar 01 2021 at 08:11):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi all,
my AFP entry stopped compiling recently
(https://ci.isabelle.systems/jenkins/job/isabelle-all/2675/) due to the
inclusion of inclusion of ML files in subdirectories. This works in
Isabelle2021.
The simplified structure is the following:
PAC_Checker
|--- ROOT
|--- ...
|--- MLton.thy
\--- code
\--- parser.sml
MLton.thy uses compile_generated_files to generate ML files, includes
parser.sml, and compile all files with MLton. This pattern now produces
the error message
Illegal path specification
"<absolute_path>/PAC_Checker/code/parser.sml" beyond base directory
I tried to declare the "code" directory in the ROOT file, but this does
not solve the error. Is there a solution that does /not/ involve moving
the ML files to the ROOT directory?
Thanks,
Mathias
Email Gateway (Mar 01 2021 at 14:43):From: Makarius <makarius@sketis.net>
On 01/03/2021 09:11, Mathias Fleury wrote:
MLton.thy uses compile_generated_files to generate ML files, includes
parser.sml, and compile all files with MLton. This pattern now produces the
error messageIllegal path specification "<absolute_path>/PAC_Checker/code/parser.sml"
beyond base directoryI tried to declare the "code" directory in the ROOT file, but this does not
solve the error. Is there a solution that does /not/ involve moving the ML
files to the ROOT directory?
There is actually something wrong on my side (after moving
Isabelle_System.copy_base_file from ML to Scala).
It should work properly now:
changeset: 73331:d045cdbdf243
tag: tip
user: wenzelm
Email Gateway (Mar 02 2021 at 07:17):From: Mathias Fleury <mathias.fleury12@gmail.com>
That works,
Thank you,
Mathias
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Apr 24 2024 at 08:20 UTC