>> Maybe the »checking« should just be a variant of the regular export. >> >> Hence the modification could be quite conservative: >> >> export_code CONSTS in LANGUAGE ( '(' OPTIONS ')' ) ( module_name NAME ) >> ( file … | ( prefix … ) ( checked ) ) >> >> where »file« denotes a relative root in the file system and »checked« >> indicated that the generated code will be checked implicitly. > > I have looked around at typical uses of 'export_code' in AFP. Most of > the time it is just informative: writing a file and looking at it in the > editor (or via the command-line!?), or doing that on the output channel. > The isabelle-export: file-system covers that already, i.e. we should be > able to eliminate almost all generated files from the AFP repository. > > So "export_code .. file" should just disappear -- it is semantically > illtyped in PIDE: editing the "file" argument will leave a trace of > machine oil spilled to the physical file-system. > > > We do need an explicit prefix and an internal check for duplicates, e.g. > as in the command 'generated_file'. > > That should be really just a prefix for the exported artifact, not the > name itself: each language processor should be smart enough to derive > file or directory names from it as required. Thus the prefix locally > belongs in front of the arguments. > > Here is an example from AFP/160ac13cdc05 > SATSolverVerification/SatSolverCode.thy: > > export_code solve > in OCaml file "code/solve.ML" > in SML file "code/solve.ocaml > in Haskell file "code/" > > It could be turned into something like this: > > export_code "code/" = solve in OCaml SML Haskell > > Some details about the automatic name derivation scheme still need to be > sorted out -- or 'file' remains as an option to specify the suffix for > effective name (without writing anything to the file-system).
Some further round of thinking. Indeed, naming files is a little bit delicate since there are two classes of target languages here: Haskell with its strict one module – one file approach and ML where source code is conceptually just a stream. Hence in the current implementation the exact interpretation of the »file« argument is up to the target language. To make this more fitting, at the moment I am thinking about something like > export_code [ ( NAME | PREFIX._ ) = ] CONSTS in LANGUAGE [ '(' OPTIONS ')' ] > [ file_prefix PATH ] [ checked ] * »checked« is just an aside to regular code generation, no distinctive variant * A mere prefix for the relative location can be given after »file_prefix«. * Language-specific options remain as they are. * The module naming schema gets more sophisticated: default, name or prefix. The key point is that this naming schema is again target-language specific. For ML: code file name default multiple structures theory name name one structure NAME NAME prefix one structure PREFIX with multiple structures PREFIX For Haskell: code file name default multiple modules module name name one module NAME NAME prefix multiple modules beneath PREFIX PREFIX module name This should cover all application cases. It will take further rounds of refinement to actually get there. At the moment I am still in favour of a diagnostic command to emit sth ad-hoc into the file system -- but this could be something separate from export_code and maybe just use $ISABELLE_TMP_PREFIX/… as destination. Just an aside: with the current tool support in Isabelle/jEdit I consider the auxiliary construct »file ‹›« obsolete – the regular exports are just two clicks away. Cheers, Florian
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev