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
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 = []}:
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
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
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
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
