Email Gateway (Aug 22 2022 at 10:33): Email Gateway (Aug 22 2022 at 10:33):From: "Achim D. Brucker" <adbrucker@0x5f.org>
Dear Isabelle Developers,
(CC Makarius and Florian - to ensure that you are aware of this email, as I assume you
are likely to be the most qualified people to advise.)
You might have seen my announcement on the Isabelle User's mailing list: I added F#
as a new target language to the code generator. This includes initial system tooling
for managing a "sandboxed" dotnet environment within Isabelle (similar to the setup
for, e.g., OCaml). The changeset is available at (I am currently trying to update
it to the latest Isabelle development version every couple of days):
https://hg.logicalhacking.com/isabelle/shortlog/feature-codegen-fsharp
The current setup successfully passes the "bin/isabelle build -a" test on Linux (well
tested) and Windows (infrequent, tests on a VM running Windows 10). Due to lack of
hardware, I cannot test it on macOS (trusting the documentation from Microsoft, the
macOS setup should work out of the box, sharing the configuration/implementation for
Linux).
I would appreciate your general opinion on F# as a new code generator target and,
in particular, your opinion and recommendations on future maintenance/development
models. I see, in principle two approaches:
1) integrating it into the main distribution of Isabelle or
2) keeping it as a separate "component" (theoretically, it could even be an AFP
entry, if users install dotnet themselves and configure the ISABELLE_DOTNET
environment variable - i.e., without the sandboxed dotnet installation)
Integrating it into the main Isabelle distribution has the advantage that the code
generator setup for F# would "live" next to the setup for the other target languages.
This could be beneficial for the future maintenance (if the setup for ML/OCaml changes,
it would be obvious that F# likely needs to be updated as well) and also would allow
for using the "ml_program_of_program" function in the structure Code_ML without duplicating
it. The disadvantage is that it adds quite some weight to the Isabelle distribution and
its release process (i.e., a non-trivial component, namely dotnet, would be added).
Keeping it separate has the advantage that it does not require any changes to the main
distribution. The disadvantage that I see is that maintenance is most likely harder
and more error-prone (in the sense of following the Isabelle development is a more
manual process) and installation for end-users is likely to be more inconvenient as
well.
I consider, personally, F# to be an interesting member of the ML-family, as it provides
a step into the world of dotnet-based frameworks and languages (as Scala opens a door
into the world of JVM-based languages and frameworks).
Thanks a lot!
Best,
Achim
PS: Just to be clear - my focus is to understand how to maintain such a component
best, and if there is interest in shipping it as a part of Isabelle itself. My
focus is not to just "throw-it-over-the-fence" and forget it (i.e., to
off-load maintenance to somebody else).
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 23 2022 at 10:50):From: Tobias Nipkow <nipkow@in.tum.de>
Achim, the code generator is part of Isabelle's trusted infrastructure. Thus I
recommend you provide your F# code generator as an AFP entry in the Tools category.
Tobias
smime.p7s
Email Gateway (Aug 23 2022 at 16:13):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Achim and Tobias &al.,
IMHO this argument on its own does not apply here. The code generator
is modular: adding another target language does not
affect existing target languages and hence does not affect their
trustworthiness, particularly not of Isabelle/ML (»Eval«)
which is at the core of all proof-replacing evaluation mechanisms.
Concerning trustworthiness in general, the code generator by its
architecture can never achieve the trustworthiness of e. g.
the LCF-style inference kernel: you are always free to configure
pointless or »unsound« things, sometimes burdening
users to come up with an appropriate »interpretation« what generated
code means in relaton to its originating theory;
a prominent example from the distribution is
HOL/Library/Code_Real_Approx_By_Float.thy.
Hence from my perspective it is difficult to argue that there are
fundamental differences between distribution
and AFP concerning trustworthiness of code generation.
From a maintenance perspective, integration into the distribution seems
actually to be the more appropriate way:
we have the tradition to setup target-language specific things in
theories where their corresponding logical
notions comes up (e. g. List.thy), and this makes things easier to
maintain and re-check across all target languages.
There might still be other issues suggesting the AFP.
Cheers,
Florian
OpenPGP_signature
Email Gateway (Aug 23 2022 at 18:28):From: Tobias Nipkow <nipkow@in.tum.de>
The code generator is sensitive. Having an external contribution in the AFP
clearly delineates what comes from the core developers and what not.
Tobias
smime.p7s
Email Gateway (Aug 25 2022 at 06:27):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Having an external contribution in the
AFP clearly delineates what comes from the core developers and what not.
That could indeed by a criterion, although it sacrifices some aspects of
maintainability.
Florian
Tobias
On 23/08/2022 18:13, Florian Haftmann wrote:
Hi Achim and Tobias &al.,
I would appreciate your general opinion on F# as a new code generator
target and,
in particular, your opinion and recommendations on future
maintenance/development
models. I see, in principle two approaches:1) integrating it into the main distribution of Isabelle or
2) keeping it as a separate "component" (theoretically, it could even
be an AFP
entry, if users install dotnet themselves and configure the
ISABELLE_DOTNET
environment variable - i.e., without the sandboxed dotnet
installation)the code generator is part of Isabelle's trusted infrastructure. Thus
I recommend you provide your F# code generator as an AFP entry in the
Tools category.IMHO this argument on its own does not apply here. The code generator
is modular: adding another target language does not
affect existing target languages and hence does not affect their
trustworthiness, particularly not of Isabelle/ML (»Eval«)
which is at the core of all proof-replacing evaluation mechanisms.Concerning trustworthiness in general, the code generator by its
architecture can never achieve the trustworthiness of e. g.
the LCF-style inference kernel: you are always free to configure
pointless or »unsound« things, sometimes burdening
users to come up with an appropriate »interpretation« what generated
code means in relaton to its originating theory;
a prominent example from the distribution is
HOL/Library/Code_Real_Approx_By_Float.thy.Hence from my perspective it is difficult to argue that there are
fundamental differences between distribution
and AFP concerning trustworthiness of code generation.From a maintenance perspective, integration into the distribution seems
actually to be the more appropriate way:
we have the tradition to setup target-language specific things in
theories where their corresponding logical
notions comes up (e. g. List.thy), and this makes things easier to
maintain and re-check across all target languages.There might still be other issues suggesting the AFP.
Cheers,
Florian
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
OpenPGP_signature
Email Gateway (Aug 25 2022 at 10:22):From: Burkhart Wolff <wolff@lri.fr>
Hm, ich wusste nicht, das nur “Developer” mit dem Prädikat
IMG (in München gewesen) Beiträge an den Isabelle Bibliotheken
leisten können sollen dürfen. Auch wenn das der Isabelle Philosophie
von Code-follows-Function zuwider läuft wie in diesem Fall.
Da erscheint Larrys Anregung, gewisse Bibliothekskomponenten
in die AFP auszulagern in einem neuen (und vielleicht unerwuenschtem) Licht.
Nun ja, schade. Um so wichtiger wird es, das die AFP zukünftig
Mechanismen hat, wie auch Isabelle Komponenten zugelassen werden
koennen. Vielleicht ist das ja in der Tat der bessere Weg.
@Makarius/Florian: Gibt es diesbezüglich Neuigkeiten ?
Sollte man eine docker-aehnliche Infrastruktur in der AFP haben ?
Liebe Grüsse aus dem sonnigen Paris,
bu
Email Gateway (Aug 25 2022 at 10:55):From: "Achim D. Brucker" <adbrucker@0x5f.org>
Hi,
Sorry for the longer answer to several aspects. Yesterday was pretty busy
for me.
On Thu, Aug 25, 2022 at 08:27:27AM +0200, Florian Haftmann wrote:
Having an external contribution in the
AFP clearly delineates what comes from the core developers and what not.
As the trustworthy argument, this is a valid argument. And, of course,
as core maintainers, you need to decide what contribution you accept or
now. I will not argue on that.
Still, as Isabelle is an Open Source project, I would have hoped that "pull requests"
(to use the github terminology) are, in principle, welcomed. Again, I am happy to commit
to maintaining it and I am also willing to invest work on bringing it up to the
required level of quality. Or maybe there is room for an 'incubator' concept (to
use Eclipse terminology), i.e., let the code generator print a warning (both in
JEdit/VSCode and the generated code) that this is an externally (less trusted)
contribution, whenever the F# target is used.
If a formal copyright transfer statement needs to be signed (e.g., to assign
copyright to TUM), I am more than happy to sign such an agreement.
That could indeed by a criterion, although it sacrifices some aspects of
maintainability.
I thought a lot about this and, frankly speaking, I have right now no idea how an
AFP entry can be maintained while, at the same time, ensuring the required
quality:
the code generator setup for Scala, OCaml, and SML is done locally in
the theories defining the formal concepts. This makes a lot of sense, as it
keeps the formal definitions and the code generator setup close together
and, by that, it is very easy to review that customized code_printings
are consistent with the formal definitions.
as the AFP does not run any generated code, an "Isabelle/F#" in the AFP
would not benefit from the "AFP as regression test" for Isabelle feature,
i.e., there would be no notifications whatsoever if changes in Isabelle
would break anything - actually worse, most likely they would not break
the F# code generation, they would just diverge silently. Also, users
will need to follow additional installations steps manually, as Isabelle
Tools cannot be distributed via the AFP.
for me, maintaining an AFP entry would essentially mean that I would need
to track all commits in the Isabelle repository and manually port changes
to an external setup that contains a "monolithic" code generator setup.
This would, IMHO, similar to the old code generator setup for Isabelle
around 2005ish, when I did my first prototype of an F# target in the context
of HOL-Testgen. I am sure there have been very good reasons why this
setup has been phased out.
Currently, by having it on a branch in the mercurial repository and providing
it as deep integration (i.e., next to the SML/OCaml setup), I have the big
benefit that I get all the updates to the SML/OCaml/Scala setup as hg commits
and hg points me rather directly to the changes (they usually pop up as merge
conflicts) and as F# is essentially a ML-dialect, updating the F# Setup only
takes a few minutes. I do not see (again, help and ideas are appreciated) how
I get a similar semi-automated setup working for setup that would be
"AFP ready".
Thus, I fear that there are only two options with a realistic maintenance workload:
either an integration into Isabelle or the distributing as patch that users need
to apply (or, of course, re-packaging a Isabelle fork). The patch/fork option is,
if course, not attractive for regular users of Isabelle.
Best,
Achim
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 25 2022 at 12:28):From: Tobias Nipkow <nipkow@in.tum.de>
I don't know who you wanted to address when you emailed "Makarius Wenzel
<isabelle-dev@in.tum.de>", but please use English on this list.
Tobias
smime.p7s
Email Gateway (Aug 25 2022 at 22:00):From: Makarius <makarius@sketis.net>
On 22/08/2022 12:32, Achim D. Brucker wrote:
You might have seen my announcement on the Isabelle User's mailing list: I added F#
as a new target language to the code generator. This includes initial system tooling
for managing a "sandboxed" dotnet environment within Isabelle (similar to the setup
for, e.g., OCaml). The changeset is available at (I am currently trying to update
it to the latest Isabelle development version every couple of days):https://hg.logicalhacking.com/isabelle/shortlog/feature-codegen-fsharp
I don't see an isolated changeset here, only a very complex history, with
branches and merges. Note that the Isabelle development model generally works
without branches (and only trivial merges): it is an easy exercise to do away
with these vices.
After some with your fork experimentation, I did manage to produce an isolated
diff like this (using your version df48d77b38f7:
hg diff --color=never -r default:feature-codegen-fsharp >
feature-codegen-fsharp.diff
The result is attached here, for the record. So it is not that complex, after all.
The current setup successfully passes the "bin/isabelle build -a" test on Linux (well
tested) and Windows (infrequent, tests on a VM running Windows 10). Due to lack of
hardware, I cannot test it on macOS (trusting the documentation from Microsoft, the
macOS setup should work out of the box, sharing the configuration/implementation for
Linux).
From my experience, macOS is never "for free". It usually works, but requires
some care and tinkering. It also require a selection of real Mac hardware for
testing: both x86_64-darwin and arm64-darwin.
Looking only briefly at your material, I did not understand where the dotnet /
F# component actually is.
De-facto, I am the universal maintainer of all multiplatform Isabelle
components. At some point, I am certainly interested to understand how F# can
be bundled, but right now is a very bad time for that --- approx. 2 weeks
before RC1 of the Isabelle2022 release.
I consider, personally, F# to be an interesting member of the ML-family, as it provides
a step into the world of dotnet-based frameworks and languages (as Scala opens a door
into the world of JVM-based languages and frameworks).
That could be true, but I have not used F# or dotnet so far.
Note that in Isabelle2022 we will have the Node.js world as a newcomer, via
VSCode and Electron. At some later stage, scala.js might follow. So we already
have a lot to digest to absorb such a huge platforms eventually.
It is still unclear to me, how far this can go.
For example, the absorption of GHC stack and OCaml opam some years ago did not
fully work out: these projects have there very own culture that does not fully
fit into Isabelle. We did not gain the stability and self-containedness of GHC
and OCaml that we were hoping for: it still requires manual tinkering
occasionally.
Makarius
feature-codegen-fsharp.diff.gz
Email Gateway (Aug 25 2022 at 22:04):From: Makarius <makarius@sketis.net>
On 22/08/2022 12:32, Achim D. Brucker wrote:
You might have seen my announcement on the Isabelle User's mailing list: I added F#
as a new target language to the code generator. This includes initial system tooling
for managing a "sandboxed" dotnet environment within Isabelle (similar to the setup
for, e.g., OCaml). The changeset is available at (I am currently trying to update
it to the latest Isabelle development version every couple of days):https://hg.logicalhacking.com/isabelle/shortlog/feature-codegen-fsharp
I don't see an isolated changeset here, only a very complex history, with
branches and merges. Note that the Isabelle development model generally works
without branches (and only trivial merges): it is an easy exercise to do away
with these vices.
After some with your fork experimentation, I did manage to produce an isolated
diff like this (using your version df48d77b38f7:
hg diff --color=never -r default:feature-codegen-fsharp >
feature-codegen-fsharp.diff
The result is attached here, for the record. So it is not that complex, after all.
The current setup successfully passes the "bin/isabelle build -a" test on Linux (well
tested) and Windows (infrequent, tests on a VM running Windows 10). Due to lack of
hardware, I cannot test it on macOS (trusting the documentation from Microsoft, the
macOS setup should work out of the box, sharing the configuration/implementation for
Linux).
From my experience, macOS is never "for free". It usually works, but requires
some care and tinkering. It also require a selection of real Mac hardware for
testing: both x86_64-darwin and arm64-darwin.
Looking only briefly at your material, I did not understand where the dotnet /
F# component actually is.
De-facto, I am the universal maintainer of all multiplatform Isabelle
components. At some point, I am certainly interested to understand how F# can
be bundled, but right now is a very bad time for that --- approx. 2 weeks
before RC1 of the Isabelle2022 release.
I consider, personally, F# to be an interesting member of the ML-family, as it provides
a step into the world of dotnet-based frameworks and languages (as Scala opens a door
into the world of JVM-based languages and frameworks).
That could be true, but I have not used F# or dotnet so far.
Note that in Isabelle2022 we will have the Node.js world as a newcomer, via
VSCode and Electron. At some later stage, scala.js might follow. So we already
have a lot to digest to absorb such a huge platforms eventually.
It is still unclear to me, how far this can go.
For example, the absorption of GHC stack and OCaml opam some years ago did not
fully work out: these projects have there very own culture that does not fully
fit into Isabelle. We did not gain the stability and self-containedness of GHC
and OCaml that we were hoping for: it still requires manual tinkering
occasionally.
Makarius
feature-codegen-fsharp.diff.gz
Email Gateway (Aug 25 2022 at 22:14):From: Makarius <makarius@sketis.net>
No, we neither have git nor pull-requests. Instead, README_REPOSITORY and the
actual hg history should tell a lot how things work.
Beyond that, it is better to discuss things with people who are responsible
for the relevant part of the Isabelle platform, before doing too much on your
own account.
Incidently, the Phabricator guys (1-3 people max.) had long texts in a similar
direction (before they had to give up eventually, not being a huge software
corporation):
https://isabelle-dev.sketis.net/book/phabcontrib/article/contributing_code
Note again that I am in release mode, so anything that is not relevant for
this release has to wait until that is published. (I am not going to
fork/branch/merge myself.)
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 25 2022 at 23:02):From: "Achim D. Brucker" <adbrucker@0x5f.org>
Hi,
On Thu, Aug 25, 2022 at 11:54:39PM +0200, Makarius wrote:
On 22/08/2022 12:32, Achim D. Brucker wrote:
You might have seen my announcement on the Isabelle User's mailing list: I added F#
as a new target language to the code generator. This includes initial system tooling
for managing a "sandboxed" dotnet environment within Isabelle (similar to the setup
for, e.g., OCaml). The changeset is available at (I am currently trying to update
it to the latest Isabelle development version every couple of days):https://hg.logicalhacking.com/isabelle/shortlog/feature-codegen-fsharp
I don't see an isolated changeset here, only a very complex history, with
branches and merges. Note that the Isabelle development model generally
works without branches (and only trivial merges): it is an easy exercise to
do away with these vices.
yes, the link goes to a "living" branch that I keep (currently) in sync with the
development repository of Isabelle. Any isolated diff can only be static, hence,
I thought that a branch is more convenient and a diff can easily obtained from it.
But I am neither a hg expert not do I know all the conventions of the Isabelle
development team.
After some with your fork experimentation, I did manage to produce an
isolated diff like this (using your version df48d77b38f7:hg diff --color=never -r default:feature-codegen-fsharp >
feature-codegen-fsharp.diffThe result is attached here, for the record. So it is not that complex, after all.
Indeed, the additions to the Isabelle code generator are not that large and also
not that complex. F# is syntax-wise a mix of ML and Ocaml. The main challenge, so
to speak, was that F# requires indentation for block structures. This is implemented
in "print_fsharp_stmt" (which is based on print_ocaml_stmt) in the structure Code_ML.
The current setup successfully passes the "bin/isabelle build -a" test on Linux (well
tested) and Windows (infrequent, tests on a VM running Windows 10). Due to lack of
hardware, I cannot test it on macOS (trusting the documentation from Microsoft, the
macOS setup should work out of the box, sharing the configuration/implementation for
Linux).From my experience, macOS is never "for free". It usually works, but
requires some care and tinkering. It also require a selection of real Mac
hardware for testing: both x86_64-darwin and arm64-darwin.
yes, this is what I fear too (while it mostly should work, the occasional
tinkering and testing will be needed). Sadly, I do lack access to this setup
right now ...
Looking only briefly at your material, I did not understand where the dotnet
/ F# component actually is.
The dotnet component (actually, the full dotnet SDK) needs to be installed using
isabelle dotnet_setup
This is similar to "isabelle ghc_setup". The ghc_setup tool (in ./lib/Tools/dotnet_setup).
I did not touch the "Admin" component part. Firstly, this really only makes sense if the F#
setup becomes integrated into the Isabelle distribution, and, secondly, the component
registration is an area of Isabelle that I do not know well).
Internally, the "dotnet_setup" tool obtains an installation script from a fixed domain provided
by Microsoft (i.e., this is promised to be a stable URL by Microsoft). There are two version of
this script: a PowerShell script for Windows and a Bash script for Linux/macOS. After downloading
this script, the "dotnet_setup" tool executes the script to install the dotnet runtime (without user
intervention) into $ISABELLE_DOTNET_ROOT (the current default value is
$ISABELLE_HOME_USER/dotnet-$ISABELLE_DOTNET_VERSION).
This is somewhat similar to the ghc/ocaml setup where stack/opam is used for installing the
actual dotnet platform (SDK). The difference is that also the installation script is obtained
"on demand" - this seems to be recommended by Microsoft to ensure that always the latest
dotnet installation script is used (the version of the dotnet framework/SDK that is actually
installed is fixed to the version specified in the Isabelle settings). If this is the
best approach for an Isabelle integration or if, e.g., integrating this install script
as a proper Isabelle component (as opam, if I understood the current setup correctly),
is something where I would love to hear your opinion on (when time permits).
F# is one of the two first-class citizen of dotnet. Hence, as soon as the dotnet SDK
is installed, F# is available (e.g., by invoking "dotnet fsi").
I hope this clarifies the questions "where the dotnet component actually is" question.
To be clear: I did not register dotnet in Admin/components. My approach is a kind of
"user installation", as I did not want to fiddle around with a part of the Isabelle
repository that I do not understand well enough to do this with the necessary level
of confidence.
De-facto, I am the universal maintainer of all multiplatform Isabelle
components. At some point, I am certainly interested to understand how F#
can be bundled, but right now is a very bad time for that --- approx. 2
weeks before RC1 of the Isabelle2022 release.
Happy to postpone the discussion to after the Isabelle 2022 release. And, again, if
there is a good technical setup allowing to maintain such a code generator configuration
outside of the Isabelle main repository - happy to hear about it.
For example, the absorption of GHC stack and OCaml opam some years ago did
not fully work out: these projects have there very own culture that does not
fully fit into Isabelle. We did not gain the stability and
self-containedness of GHC and OCaml that we were hoping for: it still
requires manual tinkering occasionally.
I do not want to hide the truth: while dotnet/F# is a stable platform that is used in
production, it has its own culture and tooling. The current setup only uses a tiny bit
of it, namely "F# interactive" (the REPL, so to speak).
Without knowing exactly how much occasional manual tinkering GHC and Ocaml require, my
best guess is that dotnet/F# would be in a similar ball park. Microsoft offers 3 years
of support for LTS releases of dotnet. Thus, some tinkering is required every 2-3 years
to switch to the latest LTS release. As the code generator setup maps to the (stable)
core of the language and does not make use of any additional libraries, this should
still fall into the "little bit of manual tinkering" category, hopefully.
Achim
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 26 2022 at 04:52):From: Tobias Nipkow <nipkow@in.tum.de>
On 25/08/2022 08:27, Florian Haftmann wrote:
Having an external contribution in the
AFP clearly delineates what comes from the core developers and what not.That could indeed by a criterion, although it sacrifices some aspects of
maintainability.
It sounds to me like this could be overcome by a well-defined interface that
allows people to add their own code generator.
Tobias
Florian
Tobias
On 23/08/2022 18:13, Florian Haftmann wrote:
Hi Achim and Tobias &al.,
I would appreciate your general opinion on F# as a new code generator
target and,
in particular, your opinion and recommendations on future
maintenance/development
models. I see, in principle two approaches:1) integrating it into the main distribution of Isabelle or
2) keeping it as a separate "component" (theoretically, it could even
be an AFP
entry, if users install dotnet themselves and configure the
ISABELLE_DOTNET
environment variable - i.e., without the sandboxed dotnet
installation)the code generator is part of Isabelle's trusted infrastructure. Thus
I recommend you provide your F# code generator as an AFP entry in the
Tools category.IMHO this argument on its own does not apply here. The code generator
is modular: adding another target language does not
affect existing target languages and hence does not affect their
trustworthiness, particularly not of Isabelle/ML (»Eval«)
which is at the core of all proof-replacing evaluation mechanisms.Concerning trustworthiness in general, the code generator by its
architecture can never achieve the trustworthiness of e. g.
the LCF-style inference kernel: you are always free to configure
pointless or »unsound« things, sometimes burdening
users to come up with an appropriate »interpretation« what generated
code means in relaton to its originating theory;
a prominent example from the distribution is
HOL/Library/Code_Real_Approx_By_Float.thy.Hence from my perspective it is difficult to argue that there are
fundamental differences between distribution
and AFP concerning trustworthiness of code generation.From a maintenance perspective, integration into the distribution seems
actually to be the more appropriate way:
we have the tradition to setup target-language specific things in
theories where their corresponding logical
notions comes up (e. g. List.thy), and this makes things easier to
maintain and re-check across all target languages.There might still be other issues suggesting the AFP.
Cheers,
Florian
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 26 2022 at 21:58):From: Makarius <makarius@sketis.net>
Thanks. From your explanations, I have learned many things about F# and dotnet.
Can you also say what your applications are?
Dotnet was once positioned as the next big thing, but recently we have seen
more excitement elsewhere (even by Microsoft): e.g. Node.js/Electron.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 28 2022 at 21:50):From: "Achim D. Brucker" <adbrucker@0x5f.org>
On Fri, Aug 26, 2022 at 11:58:17PM +0200, Makarius wrote:
Thanks. From your explanations, I have learned many things about F# and dotnet.
Can you also say what your applications are?
Hard to summarize in a few sentences. My original interest (way back in 2007, when
fiddling with mono was still required on Linux) was driven by the need to interact,
from Isabelle generated code, with Microsoft APIs for which nice packages were only
available on dotnet. Access to Microsoft tooling and APIs is still a big motivation.
England, at least the South West, seems to be in a strong grip by Microsoft, i.e.,
the Uni IT and also local project partners (mostly SMEs, which is likely also a
contributing factor) essentially require that one can interact with dotnet for joint
projects. Positively, there is also a quite strong community of F# developers/companies
(e.g., using the SAFE stack https://safe-stack.github.io/ that allows developing web
applications type-safe in F#) in England ...
Personally, it's more the "I can program in ML and have easy access to all the shiny
frameworks (via https://www.nuget.org/), a reasonable well working package manager/build
systems, and IDE support (e.g., Ionice in VSCode)" that makes it an attractive platform.
A lot of the problems I solve with F# these days are "mid-size" data processing/conversions
tasks (that other people might solve in Python).
The combination of having a strongly typed programming language with pattern matches
and also having access to databases, type providers for web scraping, and parser/validators
for many formats available as libraries is a nice sweet spot. Overall, very similar
to Scala on the Java platform. Also very similar to Scala, F# also has the "dualism" of
larger compiled programs and scripts that can directly be executed.
While there are good web-stacks for F# (that essentially require nearly no JavaScript
programming), good cross-platform UIs for desktop apps did essentially not exists
(respectively, the ones that did exist were mostly generating Node.js/Electron
applications). This seems to change right now - also Microsoft seems to see a
need for a cross-platform UI framework for dotnet.
Dotnet was once positioned as the next big thing, but recently we have seen
more excitement elsewhere (even by Microsoft): e.g. Node.js/Electron.
It's clearly not as hyped as node.js/Electron. On the other hand, upgrades of
project across major versions of the underlying framework have been less painless
for F# than for the few node.js projects I am involved with ;-).
Cheers,
Achim
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Sep 06 2022 at 07:53):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
This thread is still unsettled.
Without going into detail, at the moment I think it is best to postpone
the discussion until the next Isabelle release is published. We
definitely need Makarius have a look on the .NET components integration.
Cheers,
Florian
OpenPGP_signature
Email Gateway (Nov 04 2022 at 19:40):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
after the Isabelle release there might now be an opportunity to revive
this thread.
Meanwhile in personal conversation Tobias and me finally agreed that,
concerning code generation itself, the best solution is to follow
Achim’s original proposal and put the F# serializer into the distribution.
@Makarius – while the .NET component setup looks promising for me, I am
no expert in that area and I think we need your final judgement on this.
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature
Email Gateway (Nov 05 2022 at 22:29):From: Makarius <makarius@sketis.net>
I have spent some time with the "isabelle dotnet_setup" script by Achim and
have turned the main ideas into proper "lambda calculus for systems
programming" (aka Scala):
https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/Pure/Tools/dotnet_setup.scala;da85bffef443
The key by Microsoft documentation is here:
https://learn.microsoft.com/en-us/dotnet/core/tools/dotnet-install-script
So this is our NEWS entry in Isabelle/da85bffef443:
* System *
Example:
isabelle dotnet_setup
isabelle dotnet fsi
1 + 1;;
#quit;;
The multiplatform installation script from the Dotnet project looks fairly
robust. At least the "1 + 1" example works smoothly on all Isabelle platforms.
For the cross-platform installation of windows on linux, I have used the
"powershell" snap of Ubuntu 22.04 LTS, just for the fun of it.
So the main remaining question for Isabelle/HOL codegen support is the proper
spelling of "F#". I would say it is "Fsharp" for the Isar command syntax and
"fsharp" in plain ML names.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 05 2022 at 22:37):From: Makarius <makarius@sketis.net>
I wonder if this is also relevant, but we are not using the regular installer
here: https://learn.microsoft.com/en-us/dotnet/core/tools/telemetry
Is there anything to do, in order to disable telemetry data sent to Microsoft?
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 05 2022 at 23:10):From: Makarius <makarius@sketis.net>
I have now added this change, hoping that it is sufficient:
https://isabelle-dev.sketis.net/rISABELLE18c50ff16bbc
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Apr 23 2024 at 08:19 UTC