<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p><font size="+1">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?<br>
</font></p>
<p><font size="+1">Manuel</font><br>
</p>
<div class="moz-cite-prefix">On 14/03/2019 15:24, Lars Hupel wrote:<br>
</div>
<blockquote type="cite"
cite="mid:dde9b385-5bba-83c2-4da4-7bf0da9a0c55@in.tum.de">
<blockquote type="cite">
<pre class="moz-quote-pre" wrap="">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")
</pre>
</blockquote>
<pre class="moz-quote-pre" wrap="">
Same error also on Jenkins.
_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
</body>
</html>