[isabelle-dev] Using ML files in subdirectories for code generation
mathias.fleury12 at gmail.com
Tue Mar 2 08:17:34 CET 2021
On 01/03/2021 15:42, Makarius wrote:
> 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
> date: Mon Mar 01 15:09:57 2021 +0100
> summary: proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.);
More information about the isabelle-dev