> Does this minimal approach make any sense, and solve the imminent
> administrative problems? In particular without a decision yet about
> ISABELLE_OCAML_VERSION vs. ISABELLE_OCAML / ISABELLE_OCAMLC?
I tend to agree. Let's fix OCaml to 4.05.0 and we can figure out a good
way to upgrade after the
I have recently (eg 6a0852b8e5a8) noticed the following behaviour, although it
may be older:
I start
isabelle jedit Analysis.thy
let it run for a little bit, then double-click on some of the early theories in
the Theories panel (probably one it has processed already or is in the process
of
> In practice "their" version means a version in distant past that was the
> current one when the author was working on the session.
The reason why I suggested it was to avoid one more burden on Isabelle
developers: whoever updates the bundled OCaml version, must also adapt
whatever arrangements
> So we could provide "isabelle opam" as wrapper for something like "opam
> --root $ISABELLE_OPAM_HOME/$ISABELLE_PLATFORM64" as well as "isabelle
> opam_init" for the specific compiler version setup. Our component wiring
> would also provide ISABELLE_OCAML and ISABELLE_OCAMLC settings for the
>
On 07/06/18 09:49, Lars Hupel wrote:
>> So we could provide "isabelle opam" as wrapper for something like "opam
>> --root $ISABELLE_OPAM_HOME/$ISABELLE_PLATFORM64" as well as "isabelle
>> opam_init" for the specific compiler version setup. Our component wiring
>> would also provide ISABELLE_OCAML
>>> So we could provide "isabelle opam" as wrapper for something like "opam
>>> --root $ISABELLE_OPAM_HOME/$ISABELLE_PLATFORM64" as well as "isabelle
>>> opam_init" for the specific compiler version setup. Our component wiring
>>> would also provide ISABELLE_OCAML and ISABELLE_OCAMLC settings for
On 07/06/18 11:41, Florian Haftmann wrote:
>
> How significant is Isabelle as an integrative platform for OCaml?
So far: insignificant.
> So I would like to focus:
> * What (upcoming) maintenance challenges are we facing?
> * Are there particular applications out there which suggest more
>
> So I would like to focus:
> * What (upcoming) maintenance challenges are we facing?
There are many applications in the AFP that link generated code to
larger developments. For example, Julian Brunner recently updated the
CAVA model checker because it is not tested systematically (e.g.
nightly),
