Email Gateway (Aug 19 2022 at 09:42): Email Gateway (Aug 19 2022 at 09:42):From: "C. Diekmann" <diekmann@in.tum.de>
Hi,
I just tested Makarius' Isabelle_17-Jan-2013 testing release [1] for Linux.
(No major problems in more than 5k Lines of Theory, mostly apply
style, some Isar)
Regarding code export for Scala, why are the case objects gone?
For example
2012: final case object One extends num
2013: final case class One() extends num
Regards
Cornelius
[1] http://www4.in.tum.de/~wenzelm/test/Isabelle_17-Jan-2013/
Email Gateway (Aug 19 2022 at 09:42):From: Makarius <makarius@sketis.net>
That was a leaked test of packaging, before the start of release
candidates for Isabelle2013. In the meantime the official
Isabelle2013-RC1 was announced here
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-January/msg00096.html
including some explanations about the testing and problem reporting
procedure.
Isabelle2013-RC2 is coming soon. It is important to keep up with the RC
chain, until the official release, and avoid getting stuck with accidental
RC versions for your personal use.
Makarius
Email Gateway (Aug 19 2022 at 09:43):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Cornelius,
scala 2.10 won't accept these. You can try yourself by generating scala
code with Isabelle2012 and try to compile it under the scala version
bundled with the upcoming Isabelle2013.
If you have a more convenient solution to the problem, just tell here.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 09:43):From: "C. Diekmann" <diekmann@in.tum.de>
Hi,
thanks for the answers.
Makarius wrote:
That was a leaked test of packaging, before the start of release candidates for Isabelle2013.
I just tested on Isabelle2013-RC2. Thanks for the info.
Isabelle2013-RC2 test results:
No major issues, the only broken thing is
sledgehammer_params[isar_proof=true]
No big deal ...
Florian Haftmann wrote:
Regarding code export for Scala, why are the case objects gone?
For example
2012: final case object One extends num
2013: final case class One() extends numscala 2.10 won't accept these. You can try yourself by generating scala
code with Isabelle2012 and try to compile it under the scala version
bundled with the upcoming Isabelle2013.
I tested the following code
object Num {
abstract sealed class num
final case object One extends num
//final case class One() extends num
final case class Bit0(a: num) extends num
final case class Bit1(a: num) extends num
} /* object Num */
object Hi {
def main(args: Array[String]) = println("Hi, this is scala
"+util.Properties.versionString+" test: '"+Num.One+"'")
}
The commented version is generated by Isabelle2013-RC2.
Output: Hi, this is scala version 2.10.0 test: 'One'
Both, versions, 2012 and 2013 examples work in scala 2.10.0.
Why should scala 2.10 reject my Isabelle 2012 case objects? I can't
find my fallacy ....
Regards
Cornelius
Email Gateway (Aug 19 2022 at 09:43):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
The problems start when polymorphism comes in. Take the examples from
HOL/ex/Codegenerator_Test, there they occur definitely.
Florian
signature.asc
Email Gateway (Aug 19 2022 at 09:44):From: Steffen Juilf Smolka <steffen.smolka@in.tum.de>
Try sledgehammer_params[isar_proofs] instead. The parameter has been renamed.
Steffen
Email Gateway (Aug 19 2022 at 09:47):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Dear Cornelius,
It has been renamed, but also the underlying implementation has been improved in a number of important ways, including
1. reliable type annotations
2. proof preplay
3. proof compression (see "isar_shrink" in the manual)
4. some support for skolemization (existentials)
and various bug fixes.
The Isar proof generation feature is still experimental, but it's much less so than in 2012. We (= Steffen and I) would be happy to hear from you if you encounter problems or have success stories to share with us.
Cheers,
Jasmin
Last updated: May 07 2024 at 01:07 UTC