documentation for generated files;
authorwenzelm
Thu Apr 04 22:18:16 2019 +0200 (5 months ago)
changeset 700570403b5127da1
parent 70056 25c0ad612d62
child 70058 43acf9a457f0
documentation for generated files;
NEWS
src/Doc/Isar_Ref/Spec.thy
     1.1 --- a/NEWS	Thu Apr 04 22:17:37 2019 +0200
     1.2 +++ b/NEWS	Thu Apr 04 22:18:16 2019 +0200
     1.3 @@ -41,6 +41,13 @@
     1.4  need to provide a closed expression -- without trailing semicolon. Minor
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Commands 'generate_file', 'export_generated_files', and
     1.8 +'compile_generated_files' support a stateless (PIDE-conformant) model
     1.9 +for generated sources and compiled binaries of other languages. The
    1.10 +compilation processed is managed in Isabelle/ML, and results exported to
    1.11 +the session database for further use (e.g. with "isabelle export" or
    1.12 +"isabelle build -e").
    1.13 +
    1.14  
    1.15  *** Isabelle/jEdit Prover IDE ***
    1.16  
     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Thu Apr 04 22:17:37 2019 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Thu Apr 04 22:18:16 2019 +0200
     2.3 @@ -1188,18 +1188,102 @@
     2.4  \<close>
     2.5  
     2.6  
     2.7 -section \<open>External file dependencies\<close>
     2.8 +section \<open>Generated files and external files\<close>
     2.9  
    2.10  text \<open>
    2.11 -  \begin{matharray}{rcl}
    2.12 +  Write access to the physical file-system is incompatible with the stateless
    2.13 +  model of processing Isabelle documents. To avoid bad effects, the theory
    2.14 +  context maintains a logical ``file-system'' for generated files, as a
    2.15 +  mapping of structured file-names to content. Names need to be unique for
    2.16 +  each theory node. When exporting generated files for other purposes, the
    2.17 +  (long) theory name is prefixed for extra qualification, but there are also
    2.18 +  means to smash overlong paths. See also @{cite "isabelle-system"} for
    2.19 +  \<^theory_text>\<open>export_files\<close> within session \<^verbatim>\<open>ROOT\<close> files, together with @{tool build}
    2.20 +  option \<^verbatim>\<open>-e\<close>.
    2.21 +
    2.22 +  \begin{matharray}{rcll}
    2.23 +    @{command_def "generate_file"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
    2.24 +    @{command_def "export_generated_files"} & : & \<open>context \<rightarrow>\<close> \\
    2.25 +    @{command_def "compile_generated_files"} & : & \<open>context \<rightarrow>\<close> \\
    2.26      @{command_def "external_file"} & : & \<open>any \<rightarrow> any\<close> \\
    2.27    \end{matharray}
    2.28  
    2.29 -  \<^rail>\<open>@@{command external_file} @{syntax name} ';'?\<close>
    2.30 +  \<^rail>\<open>
    2.31 +    @@{command generate_file} path '=' content
    2.32 +    ;
    2.33 +    path: @{syntax embedded}
    2.34 +    ;
    2.35 +    content: @{syntax embedded}
    2.36 +    ;
    2.37 +    @@{command export_generated_files} (files_in_theory + @'and')
    2.38 +    ;
    2.39 +    files_in_theory: (@'_' | (path+)) (('(' @'in' @{syntax name} ')')?)
    2.40 +    ;
    2.41 +    @@{command compile_generated_files} (files_in_theory + @'and') \<newline>
    2.42 +      (@'external_files' (external_files + @'and'))? \<newline>
    2.43 +      (@'export_files' (export_files + @'and'))? \<newline>
    2.44 +      (@'export_prefix' path)?
    2.45 +    ;
    2.46 +    external_files: (path+) (('(' @'in' path ')')?)
    2.47 +    ;
    2.48 +    export_files: (path+) (executable?)
    2.49 +    ;
    2.50 +    executable: '(' ('exe' | 'executable') ')'
    2.51 +    ;
    2.52 +    @@{command external_file} @{syntax name} ';'?
    2.53 +  \<close>
    2.54 +
    2.55 +  \<^descr> \<^theory_text>\<open>generate_file path = content\<close> augments the table of generated files
    2.56 +  within the current theory by a new entry: duplicates are not allowed. The
    2.57 +  name extension determines a pre-existent file-type; the \<open>content\<close> is a
    2.58 +  string that is preprocessed according to rules of this file-type.
    2.59 +
    2.60 +  For example, Isabelle/Pure supports \<^verbatim>\<open>.hs\<close> as file-type for Haskell:
    2.61 +  embedded cartouches are evaluated as Isabelle/ML expressions of type
    2.62 +  \<^ML_type>\<open>string\<close>, the result is inlined in Haskell string syntax.
    2.63 +
    2.64 +  \<^descr> \<^theory_text>\<open>export_generated_files paths (in thy)\<close> retrieves named generated files
    2.65 +  from the given theory (that needs be reachable via imports of the current
    2.66 +  one). By default, the current theory node is used. Using ``\<^verbatim>\<open>_\<close>''
    2.67 +  (underscore) instead of explicit path names refers to \emph{all} files of a
    2.68 +  theory node.
    2.69 +
    2.70 +  The overall list of files is prefixed with the respective (long) theory name
    2.71 +  and exported to the session database. In Isabelle/jEdit the result can be
    2.72 +  browsed via the virtual file-system with prefix ``\<^verbatim>\<open>isabelle-export:\<close>''
    2.73 +  (using the regular file-browser).
    2.74 +
    2.75 +  \<^descr> \<^theory_text>\<open>compile_generated_files paths (in thy) where compile_body\<close> retrieves
    2.76 +  named generated files as for \<^theory_text>\<open>export_generated_files\<close> and writes them into
    2.77 +  a temporary directory, such that the \<open>compile_body\<close> may operate on them as
    2.78 +  an ML function of type \<^ML_type>\<open>Path.T -> unit\<close>. This may create further
    2.79 +  files, e.g.\ executables produced by a compiler that is invoked as external
    2.80 +  process (e.g.\ via \<^ML>\<open>Isabelle_System.bash\<close>), or any other files.
    2.81 +
    2.82 +  The option ``\<^theory_text>\<open>external_files paths (in base_dir)\<close>'' copies files from the
    2.83 +  physical file-system into the temporary directory, \emph{before} invoking
    2.84 +  \<open>compile_body\<close>. The \<open>base_dir\<close> prefix is removed from each of the \<open>paths\<close>,
    2.85 +  but the remaining sub-directory structure is reconstructed in the target
    2.86 +  directory.
    2.87 +
    2.88 +  The option ``\<^theory_text>\<open>export_files paths\<close>'' exports the specified files from the
    2.89 +  temporary directory to the session database, \emph{after} invoking
    2.90 +  \<open>compile_body\<close>. Entries may be decorated with ``\<^theory_text>\<open>(exe)\<close>'' to say that it is
    2.91 +  a platform-specific executable program: the executable file-attribute will
    2.92 +  be set, and on Windows the \<^verbatim>\<open>.exe\<close> file-extension will be included;
    2.93 +  ``\<^theory_text>\<open>(executable)\<close>'' only refers to the file-attribute, without special
    2.94 +  treatment of the \<^verbatim>\<open>.exe\<close> extension.
    2.95 +
    2.96 +  The option ``\<^theory_text>\<open>export_prefix path\<close>'' specifies an extra path prefix for all
    2.97 +  exports of \<^theory_text>\<open>export_files\<close> above.
    2.98  
    2.99    \<^descr> \<^theory_text>\<open>external_file name\<close> declares the formal dependency on the given file
   2.100    name, such that the Isabelle build process knows about it (see also @{cite
   2.101 -  "isabelle-system"}). The file can be read e.g.\ in Isabelle/ML via \<^ML>\<open>File.read\<close>, without specific management by the Prover IDE.
   2.102 +  "isabelle-system"}). This is required for any files mentioned in
   2.103 +  \<^theory_text>\<open>compile_generated_files / external_files\<close> above, in order to document
   2.104 +  source dependencies properly. It is also possible to use \<^theory_text>\<open>external_file\<close>
   2.105 +  alone, e.g.\ when other Isabelle/ML tools use \<^ML>\<open>File.read\<close>, without
   2.106 +  specific management of content by the Prover IDE.
   2.107  \<close>
   2.108  
   2.109