[isabelle-dev] Using ML files in subdirectories for code generation

[Mathias Fleury]

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


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20210301/4be2e4db/attachment.htm>