Stream: Beginner Questions

Topic: Export files from session database exports

view this post on Zulip David Wang (Sep 18 2025 at 15:02):

Hello,

I am trying to export code to destinations relative to the session root after modifying them with compile_generated_files. I am calling cp -r * in the where block. Is there a way to avoid this?

Thanks,

David

More info:

The folder structure:

..
| <session root>
    | ROOT
    | F1.thy
    | F2.thy

The files:

ROOT:

session Scratch = HOL +
  options [document = pdf, document_output = "output"]
  theories [document = false]
    F1
  theories
    F2
  document_files
    "root.tex"

F1:

theory F1
  imports Main
begin
definition "test x ≡ STR ''123''"

export_code test
in Eval module_name Scratch file_prefix "out"

end

F2:

theory F2
  imports F1
begin

compile_generated_files "code/out.ML" (in "F1")
export_files ‹code/out.ML› ‹text.txt›
export_prefix "d"
where  ‹fn dir =>
    let
      val exec = Generated_Files.execute dir;
      val _ = exec ‹Modify› ("echo 'println \"here\"' >> code/out.ML");

      val _  = exec ‹Make file› "touch text.txt";

      val _ = exec ‹Move outside› ("cp -r * " ^ (Path.current |> File.absolute_path |> Path.implode));
    in ()
    end
›

end

Last updated: Sep 18 2025 at 20:22 UTC