Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Using ML files in subdirectories for code ...


view this post on Zulip 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

view this post on Zulip 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 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?

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

view this post on Zulip 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: Mar 04 2024 at 10:08 UTC