[isabelle-dev] Problem with Cache_IO in Jedit
Hi,
I noticed that on my jedit build Cache_IO.run is not giving intended
result. I tested it with the attached theory file. From jedit output, I
get this result:
val it = {output = [], return_code = 1, redirected_output = []}:
Cache_IO.result
However, when the same file is run in isabelle tty mode the Cache_IO.run
function seems to work fine.
val it =
{output = [], return_code = 0, redirected_output = [Hello World!]}:
Cache_IO.result
What could be the problem?
Regards,
Harsha
theory test imports Main begin
fun add :: nat = nat = nat where
add x y = x + y
ML{*
fun make_cmd infile outfile =
/bin/cat ^ (Path.print infile) ^^ (Path.print outfile);
Cache_IO.run make_cmd (Hello World!);
*}
end
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Problem with Cache_IO in Jedit
On Sun, 24 Jul 2011, Sree Harsha Totakura wrote:
Hi,
I noticed that on my jedit build Cache_IO.run is not giving intended
result. I tested it with the attached theory file. From jedit output, I
get this result:
val it = {output = [], return_code = 1, redirected_output = []}:
Cache_IO.result
However, when the same file is run in isabelle tty mode the Cache_IO.run
function seems to work fine.
val it =
{output = [], return_code = 0, redirected_output = [Hello World!]}:
Cache_IO.result
What could be the problem?
Path.print is for human-readable output in the IDE. On the TTY you happen
to get plain text only, so it works under the asumption that there are no
spaces in the file name (which is a common source of spurious break-downs
of shell scripts). In jEdit the situation is better, since the wrong
function Path.print always includes extra markup that make this attempt
fail immediately.
The proper function in this situation is File.shell_path.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Code generation in Isabelle
On Thu, 21 Jul 2011, Lukas Bulwahn wrote: at the moment, we have two code generators in Isabelle: 1. An ancient code generator in Isabelle by Stefan Berghofer - limited to SML without supporting type classes. Commands to invoke it were code_module and code_library. 2. A generic code generator in Isabelle by Florian Haftmann - extenible to multiple target languages, supporting type classes, basic integration of reflection and abstraction mechanisms Commands to invoke it are export_code, value, code_reflect, and some others. The second subsumes the first, so we intend to remove the first code generator from the next Isabelle distribution if there are not any strong defenders of the ancient code generator. I have asked this question several years ago already, but there were a few reasons not to delete it immediately, which I have forgotten (or not fully understood in the first place). Some months ago I have renovated some really old HOL reference manual material, and moved the new version to the isar-ref. This has included the code generator, see section 10.15.2 in isar-ref of Isabelle/521de6ab277a. Apart from repainting the walls and renewing the wallpapers just before demolition, I've also observed that the old code generator is still in use in several places: some applications by Stefan Berghofer (HOL-Proofs/Lambda and Extraction, AFP/POPLmark-deBruijn), and MicroJava and its clones/descendants in AFP. Anyway, the standard procedure for removal of old stuff is to start marking it as old or legacy in the NEWS, and emitting suitable legacy_warnings. This can also mean to move the source modules to another place, like src/HOL/Library/Old_Codegen.thy in this situation. After 1 or 2 full release cycles the material is then removed altogether. Things that have been there for such a long time cannot be removed abruptly, without causing damage or confusion somewhere. Aside: On page 232 of the above-mentioned manual there is an example about const_code wfrec. The same is still used here in MicroJava: http://isabelle.in.tum.de/repos/isabelle/annotate/eee4fa79398f/src/HOL/MicroJava/J/TypeRel.thy#l100 The source says Code generator setup (FIXME!). The changelog says: no consts_code for wfrec, as it violates the code generation = equational reasoning principle (before it was in src/HOL/Wellfounded.thy). Does that mean there is something utterly wrong with MicroJava? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testing HOL/Import
On Wed, 20 Jul 2011, Florian Haftmann wrote: On Wed, Jul 20, 2011 at 11:33 AM, Alexander Krauss kra...@in.tum.de wrote: Now my question is: What do we actually know when HOL-Generate-HOLLight completes without error? Should the generated file be compared with the version in the repository and should the test fail when they are not identical? Are there other things that should be checked? I view the matter similar to our documents in doc-src: both source and generated files are included in the repository. For the documents, there is the building of the PDFs from the generated tex sources, and the generation of the tex sources from the theories (for bootstrap reasons in that order). This is due to many historical oddities. We have to live with it some more time, but should not give up moving towards plain formal document sessions uniformly, without any special tricks (such as the now obsolete rail executable as part of the process). For the importer, there is the loading of the generated files, and, only if HOL4/Light is available, the re-generation of the files. The first can happen in a regular makeall, the second in a dedicated test. The only thing to keep in mind is that before releasing the generated files should be updated manually for consistency: inconsistency can always eliminated as long as the two build steps work! In all these years I've never understood the purpose of the generation process -- generated sources are a bit like self-modifying code. Does it mean that the generation process is where the actual proofs are imported (still quite slowly for due accidental technical reasons), and the regular sessions are based on oracles only? Which purpose do the generated theory files have in the first place? The smart_string_of functions are a bit odd, reparsing not really cheap, and the result is an artificial sequentialization of the import graph. E.g. there could be a single command to load all desired theorems (with explicit proofs inside), and potentially another command to pretty print some of the content in human-readable form. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Code generation in Isabelle
On 07/24/2011 04:57 PM, Makarius wrote: On Thu, 21 Jul 2011, Lukas Bulwahn wrote: at the moment, we have two code generators in Isabelle: 1. An ancient code generator in Isabelle by Stefan Berghofer - limited to SML without supporting type classes. Commands to invoke it were code_module and code_library. 2. A generic code generator in Isabelle by Florian Haftmann - extenible to multiple target languages, supporting type classes, basic integration of reflection and abstraction mechanisms Commands to invoke it are export_code, value, code_reflect, and some others. The second subsumes the first, so we intend to remove the first code generator from the next Isabelle distribution if there are not any strong defenders of the ancient code generator. I have asked this question several years ago already, but there were a few reasons not to delete it immediately, which I have forgotten (or not fully understood in the first place). As you have asked this question several years ago, it seems like an effort that is worthwhile to be continued. Several years ago, there still were some open issues, execution of inductive predicates, executing partial functions, program extraction, which now should all be resolved -- or only minor issues remain, that could now be fixed easily. Some months ago I have renovated some really old HOL reference manual material, and moved the new version to the isar-ref. This has included the code generator, see section 10.15.2 in isar-ref of Isabelle/521de6ab277a. Apart from repainting the walls and renewing the wallpapers just before demolition, I've also observed that the old code generator is still in use in several places: some applications by Stefan Berghofer (HOL-Proofs/Lambda and Extraction, AFP/POPLmark-deBruijn), and MicroJava and its clones/descendants in AFP. I will look at these applications, and can probably replace them by new equivalent operations with the new code generator. Anyway, the standard procedure for removal of old stuff is to start marking it as old or legacy in the NEWS, and emitting suitable legacy_warnings. This can also mean to move the source modules to another place, like src/HOL/Library/Old_Codegen.thy in this situation. After 1 or 2 full release cycles the material is then removed altogether. Things that have been there for such a long time cannot be removed abruptly, without causing damage or confusion somewhere. I will follow that standard procedure, once all occurrences of the old code generator invocations are replaced. Aside: On page 232 of the above-mentioned manual there is an example about const_code wfrec. The same is still used here in MicroJava: http://isabelle.in.tum.de/repos/isabelle/annotate/eee4fa79398f/src/HOL/MicroJava/J/TypeRel.thy#l100 The source says Code generator setup (FIXME!). The changelog says: no consts_code for wfrec, as it violates the code generation = equational reasoning principle (before it was in src/HOL/Wellfounded.thy). Does that mean there is something utterly wrong with MicroJava? I will look into this issue and can report here, in the changelog, or in the NEWS about its solution. Lukas Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Code generation in Isabelle
Anyway, the standard procedure for removal of old stuff is to start marking it as old or legacy in the NEWS, and emitting suitable legacy_warnings. I will follow that standard procedure, once all occurrences of the old code generator invocations are replaced. Put in legacy warnings already now, as they will alert users who accidentially type the wrong commands (remember our experience with the methods evaluation vs. eval last week). You don't have to wait with this until all else is resolved. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
