Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Makarius]

On 14/03/2019 20:03, Lars Hupel wrote:
> 
> It initially failed because the OCaml people rely on "m4", which
> apparently is not installed by default on modern Ubuntu systems.

None of these ancient build tools are available by default on any
current OS: m4, make, etc. are all evil in some sense.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Lars Hupel]

OK. This is running now in testboard:


The corresponding changeset is
.


I have discarded my changeset now, because Florian has pushed an 
alternative solution. Here it is running:




It initially failed because the OCaml people rely on "m4", which 
apparently is not installed by default on modern Ubuntu systems.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Lars Hupel]

> Where "automatic" means that a single Isabelle administrator (e.g. the
> local user) decides to invoke "isabelle ocaml_setup" and do other
> Isabelle administration in parallel. Afterwards the ISABELLE_OCAML
> settings will be correctly provided by the etc/settings scripts, without
> any further automatisms that can fail in strange ways.

OK. This is running now in testboard:


The corresponding changeset is
.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Makarius]

On 14/03/2019 15:38, Lars Hupel wrote:
>> I don't understand what is going on here. I thought I had to set
>> ISABELLE_OCAML manually for this kind of code export to even do
>> something. From what I can tell, I did /not/ set ISABELLE_OCAML on my
>> machine, but I still get that error. Or did that behaviour change somehow?
> 
> My understanding of the problem is as follows: Florian has thankfully
> upgraded the code generator to emit code for OCaml 4.06+ with zarith.
> However, it is still unclear how to install zarith systematically (i.e.
> thread-safe but automatic).

Where "automatic" means that a single Isabelle administrator (e.g. the
local user) decides to invoke "isabelle ocaml_setup" and do other
Isabelle administration in parallel. Afterwards the ISABELLE_OCAML
settings will be correctly provided by the etc/settings scripts, without
any further automatisms that can fail in strange ways.


> For the error to be triggered I believe it is sufficient to have been
> executed "isabelle opam_setup" once.

This is not sufficient, and I have no time right now to look at the details.

For the moment I have merely disabled Isabelle OPAM and OCaml as follows
in $ISABELLE_HOME_USER/etc/settings:

  ISABELLE_OPAM_ROOT=""
  ISABELLE_OCAML=""
  ISABELLE_OCAMLC=""

That is rather brutal, but allows me to continue with the current tip
version.


Makarius



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Lars Hupel]

> I don't understand what is going on here. I thought I had to set
> ISABELLE_OCAML manually for this kind of code export to even do
> something. From what I can tell, I did /not/ set ISABELLE_OCAML on my
> machine, but I still get that error. Or did that behaviour change somehow?

My understanding of the problem is as follows: Florian has thankfully
upgraded the code generator to emit code for OCaml 4.06+ with zarith.
However, it is still unclear how to install zarith systematically (i.e.
thread-safe but automatic).

For the error to be triggered I believe it is sufficient to have been
executed "isabelle opam_setup" once.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Manuel Eberl]

I don't understand what is going on here. I thought I had to set
ISABELLE_OCAML manually for this kind of code export to even do
something. From what I can tell, I did /not/ set ISABELLE_OCAML on my
machine, but I still get that error. Or did that behaviour change somehow?

Manuel

On 14/03/2019 15:24, Lars Hupel wrote:
>> I get this failure on my regular Ubuntu 18.04:
>>
>> *** Failed to load theory "HOL-Library.Library" (unresolved
>> "HOL-Library.Finite_Map")
>> *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec"
>> ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
>> *** At command "export_code" (line 1428 of
>> "~~/src/HOL/Library/Finite_Map.thy")
> Same error also on Jenkins.
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Lars Hupel]

> I get this failure on my regular Ubuntu 18.04:
> 
> *** Failed to load theory "HOL-Library.Library" (unresolved
> "HOL-Library.Finite_Map")
> *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec"
> ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
> *** At command "export_code" (line 1428 of
> "~~/src/HOL/Library/Finite_Map.thy")

Same error also on Jenkins.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Florian Haftmann]

>> Are there any issues remaining on this thread after
>> http://isabelle.in.tum.de/repos/isabelle/rev/55534affe445 ?
> 
> I get this failure on my regular Ubuntu 18.04:
> 
> *** Failed to load theory "HOL-Library.Library" (unresolved
> "HOL-Library.Finite_Map")
> *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec"
> ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
> *** At command "export_code" (line 1428 of
> "~~/src/HOL/Library/Finite_Map.thy")
> 
> 
> ocamlexec appears to reconfigure the OPAM installation insided
> Isabelle/ML, but this is conceptually wrong as I explained already.

I would doubt that since ocamlexec is modelled following the existing
scripts ocamlc and ocaml; the only candidates for irregular activities
would be ocamlfind and ocamlopt themselves, which would be strange.

> Also note that ISABELLE_OPAM_ROOT is always provided, even it that is
> not active.

OK, this might at least explain the reproducible failure above.

Let's see what we get after the next iteration.

Cheers,
Florian



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Makarius]

On 13/03/2019 20:49, Florian Haftmann wrote:
> Are there any issues remaining on this thread after
> http://isabelle.in.tum.de/repos/isabelle/rev/55534affe445 ?

I get this failure on my regular Ubuntu 18.04:

*** Failed to load theory "HOL-Library.Library" (unresolved
"HOL-Library.Finite_Map")
*** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec"
ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
*** At command "export_code" (line 1428 of
"~~/src/HOL/Library/Finite_Map.thy")


ocamlexec appears to reconfigure the OPAM installation insided
Isabelle/ML, but this is conceptually wrong as I explained already.

Also note that ISABELLE_OPAM_ROOT is always provided, even it that is
not active.


The general model is this:

  * Administrative tools like "isabelle ocaml_setup" or "isabelle
ghc_setup" provide a local installation with sufficient information in
the target directory, such that etc/settings can work out the resulting
ISABELLE_OCAML / ISABELLE_OCAMLC or ISABELLE_GHC settings for the
underlying platform, without running any installation tools again.

  * The Isabelle/ML world only refers to these settings as consolidated
executables that don't change their own installation when invoked: many
invocations will run in parallel. Moreover this must not assume that it
is actually based on opam or stack: old-style manual installation of
ocaml/ocamlc or ghc is still allowed (we've had this discussion some
month ago concerning stack: it is just too heavy to be the only way to
refer to ghc).


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Florian Haftmann]

Are there any issues remaining on this thread after
http://isabelle.in.tum.de/repos/isabelle/rev/55534affe445 ?

Cheers,
Florian

Am 24.06.18 um 22:29 schrieb Makarius:
> On 07/06/18 15:22, Lars Hupel wrote:
>>> 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 release.
> 
> (This thread is still open.)
> 
> I presently tend to postpone the question if/how to support OCaml after
> the Isabelle2018.
> 
> 
>   Makarius
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Makarius]

On 07/06/18 15:22, Lars Hupel wrote:
>> 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 release.

(This thread is still open.)

I presently tend to postpone the question if/how to support OCaml after
the Isabelle2018.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Lars Hupel]

> 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 release.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Lars Hupel]

> 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), and the Isabelle formalization had diverged from the remaining
code.

Similarly, this also affects the "Iptables_Semantics" sessions where the
other code is kept separately. I haven't recently investigated whether
or not the generated code still compiles cleanly with the rest.

In essence, this is a "luxury problem": People are building bigger
applications with Isabelle on a wider variety of platforms, so more
things need to be tested.

> * Are there particular applications out there which suggest more
> integration with ocaml?

Simon Wimmer's timed automata formalization. I'll let him speak about
the technical details.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Makarius]

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
> integration with ocaml?

I have been thinking of why3 for Isabelle/HOL-SPARK, but with the
dependency on make, m4, gcc, the "isabelle opam" component will not make
that magically available to end-users. (We have abandomed the user-model
with "make" many years ago.)


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Florian Haftmann]

>>> 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
>>> result.
>>
>> Do you intend to provide such a component for the 2018 release?
> 
> I was asking myself the same question yesterday: anything added at this
> stage needs to have some significance.

How significant is Isabelle as an integrative platform for OCaml?  The
code generator checks have been intended as a mere device to ensure that
nothing falls into disrepair (with all consequences regarding
infrastructure maintenance), but not as a development tool by itself.

So I would like to focus:
* What (upcoming) maintenance challenges are we facing?
* Are there particular applications out there which suggest more
integration with ocaml?
* …

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Makarius]

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 and ISABELLE_OCAMLC settings for the
>> result.
> 
> Do you intend to provide such a component for the 2018 release?

I was asking myself the same question yesterday: anything added at this
stage needs to have some significance.

I have experimented a bit more with Cygwin64: its opam package pulls in
a lot of extra things, including Python. Generally, opam appears to be a
"developer" tool: it requires the canon of old-style build tools like
make, m4 etc. -- none of the OS platforms provides that by default.

So "isabelle opam" would be mainly an administrative tool: the single
"opam" executable for all platforms and a shell script around it. No
ambitions to make this generally available for regular Isabelle users.
We could put it into the "components/optional" category.


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?


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Lars Hupel]

> 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
> result.

Do you intend to provide such a component for the 2018 release?
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Lars Hupel]

> 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 developers made in the AFP to accommodate for
breaking OCaml changes.

But because that's a rather small price to pay (breaking changes are
rare), I don't have a strong opinion either way.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Makarius]

On 06/06/18 11:39, Lars Hupel wrote:
>> The opam executables only require a few MB. The result in
>> ~/.isabelle/opam above is 340 MB, for ocaml and ocamlc. This is a fair
>> investment to evade the "dynamic version hell", and normal Isabelle
>> users won't have to see it.
>>
>> 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
>> result.
> 
> That sounds reasonable. What is the reason for placing "opam" under
> "$ISABELLE_HOME_USER" (by default), though? I don't see a reason why
> this couldn't be shared with an existing installation.

I've misunderstood the "opam init --comp" procedure, with its tendency
towards a single version. With "opam switch install" it is possible to
install arbitrary (disjoint) versions, so indeed we can reuse the
central ~/.opam root (with the minor disadvantage that it appears to
assume just one OS platform, i.e. the HOME cannot be shared among
platforms).


> Would it be possible to specify the concrete compiler as a system
> option? The big benefit there is that it would decrease maintenance
> burden: session authors could select their "ocamlc" version in "options
> [...]". It means people who have custom OCaml code printing (like Simon)
> don't have to care about a hard-coded "4.05.0" somewhere; they'll get a
> consistent setup regardless.

In practice "their" version means a version in distant past that was the
current one when the author was working on the session.

I was more thinking of one standard OCaml version for a particular
Isabelle version, which could be just ISABELLE_OCAML_VERSION in
etc/settings. Multiple Isabelle versions can take this from a central
~/.opam store to produce ISABELLE_OCAML and ISABELLE_OCAMLC, but within
each Isabelle version it should be a constant, not a variable.

This conforms with the idea of Isabelle components: we include one fixed
version for each tool, such that everything fits nicely together.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Lars Hupel]

> I have now experimented a bit with opam-1.2.2 on Linux, Mac OS X,
> Windows/Cygwin64. It appears to work quite well, e.g. like this:
> 
>   ./opam-1.2.2-x86_64-Darwin init --root ~/.isabelle/opam --comp 4.05.0
> 
> The opam executables only require a few MB. The result in
> ~/.isabelle/opam above is 340 MB, for ocaml and ocamlc. This is a fair
> investment to evade the "dynamic version hell", and normal Isabelle
> users won't have to see it.
> 
> 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
> result.

That sounds reasonable. What is the reason for placing "opam" under
"$ISABELLE_HOME_USER" (by default), though? I don't see a reason why
this couldn't be shared with an existing installation.

Would it be possible to specify the concrete compiler as a system
option? The big benefit there is that it would decrease maintenance
burden: session authors could select their "ocamlc" version in "options
[...]". It means people who have custom OCaml code printing (like Simon)
don't have to care about a hard-coded "4.05.0" somewhere; they'll get a
consistent setup regardless.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Makarius]

On 30/05/18 11:15, Lars Hupel wrote:
>> The best way maybe is to introduce a dedicated isabelle tool »ocamlc«
>> which uses an environment parameter ISABELLE_OCAML as path prefix to
>> ocamlc / ocamlfind; this would be more pleasant than any kind of ad-hoc
>> montage in ML.
> 
> Yes, but we would still need to figure out how to "peg" a particular
> OCaml version. As far as I understand there is now way to make this
> change that will work for both 4.06+ and before.
> 
> Maybe we could bundle OPAM, which is a tool that is able to download and
> install a particular OCaml version on all the platforms that Isabelle
> also supports.

I have now experimented a bit with opam-1.2.2 on Linux, Mac OS X,
Windows/Cygwin64. It appears to work quite well, e.g. like this:

  ./opam-1.2.2-x86_64-Darwin init --root ~/.isabelle/opam --comp 4.05.0

The opam executables only require a few MB. The result in
~/.isabelle/opam above is 340 MB, for ocaml and ocamlc. This is a fair
investment to evade the "dynamic version hell", and normal Isabelle
users won't have to see it.

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
result.


There might be further consequences of such a move: the opam universe
provides packages for alt-ergo, coq, why3, which are potentially useful
tools to be integrated with Isabelle eventually.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Lars Hupel]

> The best way maybe is to introduce a dedicated isabelle tool »ocamlc«
> which uses an environment parameter ISABELLE_OCAML as path prefix to
> ocamlc / ocamlfind; this would be more pleasant than any kind of ad-hoc
> montage in ML.

Yes, but we would still need to figure out how to "peg" a particular
OCaml version. As far as I understand there is now way to make this
change that will work for both 4.06+ and before.

Maybe we could bundle OPAM, which is a tool that is able to download and
install a particular OCaml version on all the platforms that Isabelle
also supports.

I'm mentioning this because I'm going to have to do a similar thing
anyway (eventually!) in order to ensure a consistent installed version
of OCaml on all the various testing machines. The reason I found this
out was that Homebrew gave me an upgrade to 4.06 which broke it, but
Ubuntu 18.04 LTS is still on 4.05.

> Btw. Zarith is available at least since Ubuntu 16.04. as package
> libzarith-ocaml.  It is anyway still unsatisfactory that such a
> fundamental concept as proper integers does not work out-of-the-box

It might be worth looking at HOL Light to see how they do it.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Florian Haftmann]

> No matter whether we decide to stick with Num or migrate to Zarith, the
> code generator needs to be updated to not link against "nums.cma" directly:
> 
>   val compile_cmd =
> "\"$ISABELLE_OCAMLC\" -w pu -o " ^ File.bash_path compiled_path ^
> " -I " ^ File.bash_path path ^
> " nums.cma " ^ File.bash_path code_path ^ " " ^ File.bash_path
> driver_path
> File.bash_path code_path ^ " " ^ File.bash_path driver_path
> 
> This is wrong, because it's not guaranteed where "nums.cma" is. The
> recommendation is to use "ocamlfind" instead. "ocamlfind" would be an
> extra dependency people would have to install, but a cursory search
> reveals that there are system packages for all major Linux
> distributions, macOS, and Cygwin.
> 
> Any thoughts on how to deal with this?

The best way maybe is to introduce a dedicated isabelle tool »ocamlc«
which uses an environment parameter ISABELLE_OCAML as path prefix to
ocamlc / ocamlfind; this would be more pleasant than any kind of ad-hoc
montage in ML.

Btw. Zarith is available at least since Ubuntu 16.04. as package
libzarith-ocaml.  It is anyway still unsatisfactory that such a
fundamental concept as proper integers does not work out-of-the-box

But there is now a possibility to have proper strings:
https://caml.inria.fr/pub/docs/manual-ocaml/libref/String.html

Maybe all these issues at a glance justify to modernized OCaml code
generation.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev