On Sun, 24 Jul 2011, Alexander Krauss wrote:
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
On 07/25/2011 10:25 AM, Makarius wrote:
On Sun, 24 Jul 2011, Alexander Krauss wrote:
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
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
Hello all,
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
On 07/21/2011 04:25 PM, Steven Obua wrote:
Actually, there is a third code generator hidden somewhere in
Isabelle.
If you are talking about what I know under the name Compute Oracle,
then rest assured that it is hidden well enough that the chance of some
user accidentially confusing it with
Lukas already assured me of that. No worries here.
- Steven
On 22.07.2011, at 00:07, Alexander Krauss wrote:
On 07/21/2011 04:25 PM, Steven Obua wrote:
Actually, there is a third code generator hidden somewhere in
Isabelle.
If you are talking about what I know under the name Compute