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

Mathias Fleury mathias.fleury12 at gmail.com
Mon Mar 1 09:11:26 CET 2021

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 

The  simplified structure is the following:


    |--- 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?



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

More information about the isabelle-dev mailing list