Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] RC3: F# not mentioned in Isabelle overview


view this post on Zulip Email Gateway (Aug 12 2023 at 19:17):

From: Wolfgang Jeltsch <wolfgang@well-typed.com>
Hi!

I just saw at https://isabelle.in.tum.de/website-Isabelle2023-RC3/ that
Isabelle has now support for F#. Does this mean that F# code can be
generated from Isabelle code? If yes, F# should perhaps be mentioned at
https://isabelle.in.tum.de/website-Isabelle2023-RC3/overview.html, where
still only SML, OCaml, Haskell, and Scala are listed as code generation
targets.

All the best,
Wolfgang

view this post on Zulip Email Gateway (Aug 12 2023 at 20:54):

From: Makarius <makarius@sketis.net>
That was the plan several months ago, but neither Achim Brucker nor Florian
Haftmann made any moves towards something fit for the release.

All we have in Isabelle2023 is an Isabelle/Scala command-line tool to download
F# for arbitrary target platforms.

(Maybe I should make the announcement less prominent, to avoid confusion.)

Makarius

view this post on Zulip Email Gateway (Aug 14 2023 at 13:12):

From: "Achim D. Brucker" <adbrucker@0x5f.org>
Hi,
Sadly the timing did not work out. I am still maintaining a (local)
Isabelle branch that includes the F# code generator (and also sync
it more or less regularly with the upstream development). The
current version makes already use of the dotnet tool integration
Makarius provides (Thanks!),.

After the release of Isabelle 2023, I plan to

Best,
Achim

view this post on Zulip Email Gateway (Aug 31 2023 at 06:35):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi,

sorry for the delayed response.

There are no longer any concerns I am aware of to include the updated
patch into the distribution (post-release).

Cheers,
Florian

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature

view this post on Zulip Tobias Heindel (Heliax GmbH) (Mar 07 2024 at 17:14):

Email Gateway said:

From: Wolfgang Jeltsch <wolfgang@well-typed.com>
Hi!

I just saw at https://isabelle.in.tum.de/website-Isabelle2023-RC3/ that
Isabelle has now support for F#. Does this mean that F# code can be
generated from Isabelle code? If yes, F# should perhaps be mentioned at
https://isabelle.in.tum.de/website-Isabelle2023-RC3/overview.html, where
still only SML, OCaml, Haskell, and Scala are listed as code generation
targets.

All the best,
Wolfgang

Also, though I am still just new to code generation, which version of Scala does the generated code comply with ?


Last updated: Apr 29 2024 at 01:08 UTC