[isabelle-dev] Using ML files in subdirectories for code generation
makarius at sketis.net
Mon Mar 1 15:42:55 CET 2021
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:
date: Mon Mar 01 15:09:57 2021 +0100
summary: proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.);
More information about the isabelle-dev