On 14/01/2019 20:20, Florian Haftmann wrote: > >> * Are there remaining uses of 'file' with empty name? Is the virtual >> file-system browser sufficiently convenient to inspect results >> interactively? > > I checked the file system browser and would be quite content with it; as > a bonus you can then make use of the syntax highlighting of jEdit (OCaml > seems not be built-in, though). > > But I want to excite more feedback of users.
Here is some feedback from myself as a user: the new stateless model to generate files works well, in particular the file-browser of Isabelle/jEdit helps. There was only a technical problem it that should no longer occur in practice, see changeset: 69696:9fd395ff57bc user: wenzelm date: Sun Jan 20 21:26:15 2019 +0100 files: Admin/components/components.sha1 Admin/components/main src/Tools/jEdit/patches/vfs_manager description: avoid crash of jEdit.closeBuffer() via TaskManager.instance.waitForIoTasks() due to race condition of save() vs. automatic load() of already open buffer, e.g. relevant for save-as on "isabelle-export:" artifacts; In the mainstream this would probably be called a "fix", but the conceptual problem behind it is still there: there are concurrent tasks that are just concatenated in sequence, without taking the nesting of the program structure into account. Proper futures are required instead of slightly odd wait operations. >> * How to specify proper (unique) export names: PIDE still lacks a >> check for uniqueness of export names, but overwriting existing exports >> is considered illegal. The 'file' allowed to produce separate names in >> the past, but it has a different meaning now (and is a candidate for >> deletion). > > Well, if we re-consider the syntax, we will also find a way for this. > >> Maybe 'export_code' should be renovated replaced by reformed commands >> like this: >> >> * "code_export PREFIX = CONSTS in LANGUAGE" where the PREFIX is >> optional and the default something like "generated" or "code". This >> could be a "thy_decl" command that updates the theory context by >> generated files that are accessible in Isabelle/ML, in addition to the >> export; it would also include a check for duplicate names. >> >> * "code_checking CONSTS in LANGUAGE" -- observing that "export_code >> ... checking" is actually a different command. It would be a "diag" >> command as before (this is relevant for parallelism). > > 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). Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev