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

[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

[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] Fwd: [Isabelle-ci] Build failure in Isabelle (benchmark)

[Lars Hupel]

"Unable to increase stack" is one of the various messages that tells
you that PolyML has run out of resources. It doesn't really tell you
what the problem is though. It might be an actual problem or a
temporary problem caused by a machine being overloaded.


This is likely connected to the recent change of platform. I will 
investigate this; maybe bumping the memory limit will resolve it.


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

Re: [isabelle-dev] NEWS

[Lars Hupel]

Or maybe as implicit part  of

isabelle ocaml_setup


Sure, that could also work.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS

[Lars Hupel]

  isabelle ocaml_opam install zarith


This should ideally happen on-the-fly from within Isabelle/ML.

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

Re: [isabelle-dev] Current AFP problems

[Lars Hupel]

> I’m getting no alerts for some reason 

I don't see any mail delivery issues in the logs. Maybe none of your
sessions were affected?

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

Re: [isabelle-dev] Towards Poly/ML 5.8

[Lars Hupel]

After a lot of refinements by David Matthews we are moving towards the
new Poly/ML 5.8 release. Isabelle/8c587dd44f51 already bundles a 
Poly/ML

version of that number, without being official yet. The Isabelle NEWS
already talk about an official release:


Is it intentional that the system identifier is still 5.7.1?

  ML_SYSTEM=polyml-5.7.1

This also raises the question if that variable has any remaining uses.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Timeouts in Flyspeck_Tame

[Lars Hupel]

Is this related to the latest Poly/ML changes? The "slow" job still runs
on the x86_64 platform. Last time it worked was 76fbd806ebc5. Hardware
is 8-core LRZ VM.

https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/1010/consoleFull
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Lars Hupel]

> The standard approach for the latter is to have the other tool directly
> import its source format into the theory context within Isabelle/ML,
> without the intermediate theory source. Doing this carefully, would even
> produce nice PIDE markup for the original sources. PIDE is an IDE for
> arbitrary user-defined languages.
> 
> It might be worth doing this for tools like Lem eventually, but I have
> not looked at it closely so far.

Lem is implemented in OCaml, so this seems like a stretch. I'd say
importing HOL4 into Isabelle is a more plausible solution.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Lars Hupel]

> What are the remaining uses of these? How much of this can be integrated
> into the formal Isabelle session? How much of it is actually obsolete?

Hard to tell from a distance, but here's what I gather from reading the
Makefiles:

– Formal_SSA appears to download some file, unpack it, and compile
generated code together with it.

– Lightweight_Java generates an Isabelle theory file with Ott.

– Buchi_Complementation compiles generated code with MLton.

– Sturm_Sequences produces some extra LaTeX documentation. The generated
PDF is even committed to the AFP.

>   * no generated files in the repository (these are not sources but
> results from sources)

What about generated theory files? This also affects the CakeML entry. I
could easily package Lem as a component, but how would "isabelle build"
call it?
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Lars Hupel]

> In 2012 we eliminated all Makefiles from AFP: I did not know that some
> came back, or chose to ignore it.

~/work/afp (default)$ find thys/ -name Makefile
thys/Buchi_Complementation/code/Makefile
thys/Formal_SSA/Makefile
thys/LightweightJava/ott-src/Makefile
thys/Sturm_Sequences/guide/Makefile

> The formal status of sessions is defined via "isabelle build" -- that is
> a powerful tool that can do many things. I.e. we can easily define that
> anything outside of it as outside of AFP.

This is the de-facto situation, yes.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Lars Hupel]

> 1. Gratchk is a similar use-case, where I need to export code, link it
> with some external ML code using MLton b/c it's faster, and test the
> result for timing regressions. Because gratchk is also bundled with
> gratgen, which is implemented in C++, I have not yet put it into the
> AFP, b/c that would mean to separate gratchk from gratgen, or to push
> C++ code to the AFP, for which I cannot expect an build infrastructure
> there.
> 
> 2. In the AFP, there is the CAVA model checker. It also comes with some
> external ML code. I just checked, and this external ML code is already
> severely bit-rotten, as it has not been maintained for years now ... at
> latest the recent string-literal reform should have reliably killed it.
>  
> Also, timing regression tests are important when doing such reforms as
> the above-mentioned string-literal reform, which has the potential to
> severely slowdown the generated code.

This is not a new problem. It is merely slightly exacerbated by making
it more difficult to run such tests manually. There have been various
discussions about this in the past, but they are all orthogonal to the
issue of code generation.

It would like to reiterate that the technical part of this issue is the
easy bit. The difficult bit is deciding policy: Should Isabelle
committers be responsible for breakage in downstream artifacts? In other
words, should the AFP stability guarantees be extended? Right now we
have that odd situation where extra sources are present (e.g. Makefiles)
but nobody bothers to look at them.

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

Re: [isabelle-dev] State of the art in Isabelle with OCaml, opam and zarith

[Lars Hupel]

> But ocamlfind semms not to provide a subcommand to invoke the
> interactive OCaml toplevel.  What am I missing?

The other way round. "ocamlfind" hooks into the toplevel.

$ isabelle ocaml_opam config exec ocaml
OCaml version 4.05.0

# #use "topfind";;
- : unit = ()
Findlib has been successfully loaded. Additional directives:
  #require "package";;  to load a package
  #list;;   to list the available packages
  #camlp4o;;to load camlp4 (standard syntax)
  #camlp4r;;to load camlp4 (revised syntax)
  #predicates "p,q,...";;   to set these predicates
  Topfind.reset();; to force that packages will be reloaded
  #thread;; to enable threads

- : unit = ()
# #require "zarith";;
/home/lars/.isabelle/opam/4.05.0/lib/zarith: added to search path
/home/lars/.isabelle/opam/4.05.0/lib/zarith/zarith.cma: loaded
# Z.one;;
- : Z.t = 

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

Re: [isabelle-dev] State of the art in Isabelle with OCaml, opam and zarith

[Lars Hupel]

It is admittedly a complicated incantation, but here you go:

$ cat test.ml
let x = Z.one;;
let _ = print_endline (Z.to_string x);;

$ isabelle ocaml_opam config exec ocamlfind -- ocamlopt -package zarith
-linkpkg test.ml

$ ./a.out
1

You need "ocamlfind" to tell the OCaml compiler ("ocamlopt") where to
look for packages.

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

Re: [isabelle-dev] mercurial accident

[Lars Hupel]

> The problem behind this: Angeliki got administrative push-access to the
> Isabelle repository, without anybody at Cambridge showing her how to use it.

Before we start blaming individual people, this is not a person problem,
but a tooling problem. Industry has figured out this problem years ago.
One doesn't simply allow pushes to master (or "default" in Mercurial).
CakeML has adopted this too.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] mercurial accident

[Lars Hupel]

> Strip the accidental changes from the repository?

Never strip public changesets.

> Back out the changes?

You can't really back out merges, as far as I know.

> Or do a no-op merge from a successor of the last working version?

This is also not possible, I think.

Do this instead:

$ hg revert -a -r 56acd449da41
$ hg commit -m "revert to 56acd449da41"

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

Re: [isabelle-dev] NEWS: Support for Isabelle command-line tools defined in Isabelle/Scala

[Lars Hupel]

* Support for Isabelle command-line tools defined in Isabelle/Scala.
Instances of class Isabelle_Scala_Tools may be configured via the shell
function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
component).


This is nice! Anything on the radar to automate compilation as well, 
just like `jedit -bf`, but for arbitrary components? That would be very 
useful for the AFP.

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

Re: [isabelle-dev] NEWS: support for GHC

[Lars Hupel]

> The binary provided by Homebrew does not exhibit that problem. I have no
> other information beyond that.

I'm trying out a High Sierra Mac Book Pro, and Stack appears to work there.

Interestingly enough, I get Poly/ML warnings of the form:

14:11:19 poly(50366,0xb042) malloc: *** mach_vm_map(size=8388608)
failed (error code=3)
14:11:19 *** error: can't allocate region
14:11:19 *** set a breakpoint in malloc_error_break to debug

This happens during the build of "HOL-Decision_Procs", which succeeds
regardless:

14:11:19 Finished HOL-Decision_Procs (0:05:36 elapsed time, 0:10:40 cpu
time, factor 1.91)

The timestamp suggests that this happens close to the end of the
session; although no heap image has to be saved for that session.

I'll run some more experiments to figure out if this is spurious or not.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: support for GHC

[Lars Hupel]

> Can you actually explain the problem and its solution?

The problem appears to be that the official Stack binaries do not work
consistently on El Capitan. The machine I've tried them on is fully
updated and has no special software setup.

The binary provided by Homebrew does not exhibit that problem. I have no
other information beyond that.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: support for GHC

[Lars Hupel]

> On an El Capitan system, this produces the following error:

The problem can alternatively be solved by installing Homebrew's stack
version and declaring

ISABELLE_STACK="/usr/local/bin/stack"

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

Re: [isabelle-dev] NEWS: support for GHC

[Lars Hupel]

> * Support for Glasgow Haskell Compiler via command-line tools "isabelle
> ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack".
> Existing settings variable ISABELLE_GHC is maintained dynamically
> according the state of ISABELLE_STACK_ROOT and ISABELLE_STACK_RESOLVER.

On an El Capitan system, this produces the following error:

$ uname -a
Darwin macisa1.in.tum.de 15.6.0 Darwin Kernel Version 15.6.0: Mon Aug 29
20:21:34 PDT 2016; root:xnu-3248.60.11~1/RELEASE_X86_64 x86_64

$ ./bin/isabelle ghc_setup
/Users/hupel/workspace/isabelle/lib/scripts/getfunctions: line 1: 31569
Illegal instruction: 4  env STACK_ROOT="$(platform_path
"$ISABELLE_STACK_ROOT")" "$ISABELLE_STACK" "$@"

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

[isabelle-dev] Slaying the hydra

[Lars Hupel]

Yesterday, Tobias observed an interesting problem:

$ hg pull
pulling from http://isabelle.in.tum.de/repos/testboard/
searching for changes
abort: HTTP Error 414: Request-URI Too Long

The cause is a combination of that repository being many-headed and
Mercurial trying to be too smart about pulling via HTTP(S).

I checked the situation and there were >400 heads in that repository. I
cleaned those and wanted to post the relevant command for posterity here:

hg strip -r "all() and not ancestors(revision_to_keep)"

Note that this is apparently not an atomic operation! During my
experiments at home interrupting a strip operation was more likely than
not to leave the repository in a corrupted state.

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

Re: [isabelle-dev] System migration

[Lars Hupel]

> I will update as soon as the migration is completed.

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

[isabelle-dev] System migration

[Lars Hupel]

Dear Isabelle developers and users,

we will perform a large-scala system migration over the next 24–48
hours. The purpose is to move towards the latest Ubuntu 18.04 LTS.

Affected will be continuous integration, the AFP, and the AFP submission
service.

Expect intermittent unavailability and HTTPS errors.

I will update as soon as the migration is completed.

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

Re: [isabelle-dev] NEWS: support for OCaml / OPAM

[Lars Hupel]

>   * How to re-init the opam installation, e.g. after changing
> ISABELLE_OCAML_VERSION (maybe even in ISABELLE_HOME_USER/etc/settings)?
> (Presently I have just removed purged ISABELLE_OPAM_ROOT.)

I don't think purging the directory is necessary. It should work out of
the box. According to my experiments, opam will just install another
OCaml version side-by-side.

>   * Is the update of ~/.ocamlinit that is proposed by opam init required?

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

Re: [isabelle-dev] AFP/HLDE

[Lars Hupel]

> For the ROOT entry there is already 'export_files' in Isabelle2018. This
> could be augmented by something like:
> 
>   export_action NAME = SCALA
> 
> with a snippet of Scala source that is a function from the resulting
> session build to unit. It could invoke build tools for Haskell, Ocaml,
> Scala, SML, even LaTeX in Isabelle/Scala.

Let's call this facility "build actions" for simplicity.

The current approach of "export_code ... checking" is, in my opinion, a
sweet spot. It can be kept working with modest effort. It doesn't test a
whole lot of things though. Making opam and stack available will help us
in the medium term by abstracting exactly what is needed for raw code
generation away from distributions.

The question about build actions is: do they solve the problem in the
AFP, e.g. with HLDE? Invoking arbitrary build tools (i.e. running
arbitrary code) is a problem for two reasons:

– A consistent environment where everything that's needed for any given
application is very hard to guarantee. The closest technologies we have
for that are currently Nix and Docker. (It's no coincidence that Nix
uses "closure" terminology.)

– What are the maintenance guarantees? If something breaks in the
generated code, violating assumptions from third-party code, who will
fix it?

As a case study, consider the "Iptables_Semantics" entry. It produces
non-trivial amounts of code that is subsequently decorated with
hand-written Haskell code that requires ~5 third-party packages.
Currently, all of this is kept in a separate repository. Assume for a
moment that this were to move into the AFP. Now, also assume evolution
of the Isabelle system (for example, some code printing). Things will
break. Furthermore, without additional efforts, this can't just build on
arbitrary machines (not even Stack fixes that fully).

But it gets worse. Let's consider another case study. Peter's GRAT
checker is currently only available in the IsaFoL repository:
. This project
consists of an Isabelle part and a C part. The latter is built with CMake.

Again – hypothetically – assume that Peter submits this to the AFP,
using build actions. He'd write something like:

  export_action tool =
Isabelle_System.bash("cmake . && make && make install")

This is going to be a nightmare. There's virtually nothing you can
assume about the C/C++ toolchain that's present on any given system. In
Haskell/Scala/OCaml one can at least install packages without root
privileges, but not in C.

Docker could fix that. But then we're back at the ever-looming question
of maintenance.

To summarize: The above is, at best, a weak argument against build
actions in general. But I think it is a strong argument against build
actions in the AFP.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] NEWS: CakeML compiler

[Lars Hupel]

This refers to AFP/c245a746483a and Isabelle/337b8ce5ff8d.

The CakeML compiler is now available from within Isabelle/ML.

Steps to use:

1) echo 'init_components "$HOME/.isabelle/contrib" 
"$ISABELLE_HOME/Admin/components/cakeml"' >> ~/.isabelle/etc/settings

2) echo 'ISABELLE_CC=gcc' >> ~/.isabelle/etc/settings
   (or clang, if you like)
3) isabelle components -a
4) import "CakeML.CakeML_Compiler" [*]
5) the command "cakeml" with the flags "literal" and "prog" is available

Examples:

cakeml (literal) ‹print "hi1";› (* prints "hi1" *)
cakeml (literal) ‹print "hi2";› (* prints "hi2" *)

(* this defines a HOL term that corresponds to a CakeML AST *)
definition simple_print :: Ast.prog where
"simple_print =
  [Ast.Tdec (Ast.Dlet default_loc Ast.Pany (Ast.App Ast.Opapp [Ast.Var 
(Short ''print''), Ast.Lit (Ast.StrLit ''hi'')]))]"


cakeml (prog) ‹simple_print› (* prints "hi" *)

How it works:

The bootstrapped CakeML compiler is available as a component that 
provides binaries for Linux and macOS. The steps to compile a CakeML 
program are as follows:


1) use "cake" to produce an assembly file "foo.S" from some input 
"foo.ml"
2) use "ISABELLE_CC" to compile the "basis_ffi.c" file to "basis_ffi.o" 
(provided by the CakeML component)

3) use "ISABELLE_CC" to link "basis_ffi.o" and "foo.S"

"cakeml (literal)" will take a cartouche that contains a literal CakeML 
program and invokes those steps.


"cakeml (prog)" will take a term. That term is evaluated through the 
code generator -- expecting a CakeML AST --, and then converted into a 
string. It will then do the same as above. The conversion into a string 
is very rudimentary at the moment. It only supports a tiny fraction of 
the CakeML abstract syntax.


Let me know if you run into any problems.

[*] Note that that theory is _not_ built when building the AFP unless 
the CakeML component is enabled and "ISABELLE_CC" is set. In a way, it's 
similar to the various "export_code ... checking" theories.

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

Re: [isabelle-dev] NEWS: discontinued old-style inner comments

[Lars Hupel]

> There were a few remaining uses in AFP. Notable changes are
> AFP/58b893c52562 and AFP/bf2659bf0a46, where I had to edit sources
> generated by LEM (!). I don't know how LEM is maintained: it needs to
> produce different inner comments next time, and can actually use
> \ CARTOUCHE notation uniformly for inner and outer comments --
> also note that this needs to be LaTeX-conformant, e.g. by another nested
> cartouche or \<^verbatim>CARTOUCHE.

The way this works is that I'll have to send them a patch. This should
hopefully be simple enough.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] CakeML compiler in the AFP

[Lars Hupel]

> Just a side-remark: Fabian Immler has started with some experiments to
> use HOL4 with CakeML inside Isabelle. You should keep in contact with
> him about progress and possibilities.

Of course. I'm aware and we're emailing back and forth.

But this is to some extent orthogonal to Fabian's efforts. This is about
packaging the already-bootstrapped CakeML compiler. If Fabian's work
will eventually be able to produce such an artifact too, all the better!
But when it does, we'll still want to have it as a packaged component,
because bootstrapping takes ages (~ 2 days).
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] CakeML compiler in the AFP

[Lars Hupel]

> What is the meaning for "optional?" for AFP?

We don't have any established process for additional components in the
AFP. The question is, should this go into "$AFP_BASE/etc/components" or not?

> I've briefly tried cake-x64-64 on Linux, Mac OS X 10.10, and Cygwin 64
> from https://isabelle.sketis.net/cygwin_2018 -- only the latter causes
> some odd problems in the first attempt ("./cake.exe: cannot execute
> binary file: Exec format error"); it might disappear after some more
> tinkering. In the worst case, such an optional tool is not available for
> Windows users.

Ramana has informed me that the .S file makes some assumptions about
Unix-y behaviour. So it's not surprising to at least one person. Michael
Norrish reported that it works on WSL.

> Providing the already compiled binaries via some component also avoids
> the still open problem of Isabelle sessions that write to the
> file-system as a side-effect: recall that we are in the process to
> eliminate that an turn it into managed "exports" instead, but that does
> not quite fit with executables.

Combined with the other arguments, there seems to be no good reason to
not have it as a component. I'll try to get this done.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] CakeML compiler in the AFP

[Lars Hupel]

Dear list,

I'm considering putting the entire CakeML compiler somewhere so that it
is accessible in the AFP. This includes a pretty-printer of (a small
subset of) the abstract syntax; together with some ML code that allows
one to invoke the compiler, not unlike "export_code ... checking".

Note that this is not yet the full compilation toolchain from
Isabelle/HOL to CakeML! It's just the tiny backend part where a CakeML
AST can be compiled by the official CakeML compiler.

I would do so without writing this to the list, but there are some
obstacles. The major obstacle being that the CakeML compiler is not in
fact a piece of ML code, but a large assembly artifact (65 MB
uncompressed) that needs to be linked to some FFI code [0]. Hence, it
requires a C compilation toolchain including "make" [1].

I see two ways forward:

1) It becomes a component.
   a) ... in Isabelle (optional)
   b) ... in the AFP (optional?)

2) The compressed artifact (~ 2 MB with xz) is committed to the AFP and
compiled on-the-fly.

I don't have a strong opinion either way. Thoughts?

Cheers
Lars


[0] The original download can be found here:


[1] Luckily the "Makefile" is so simple that I am attaching it below in
full:

cake: cake.o basis_ffi.o

clean:
rm -f cake.o basis_ffi.o cake

.PHONY: clean

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

[isabelle-dev] datatype_compat: exception Bind

[Lars Hupel]

Dear BNF developers,

it appears that the "datatype_compat" cannot cope with non-standard
bindings. I get an "exception Bind" when trying to invoke
"datatype_compat" on a "qualified" or "private" datatype. There's a
somewhat satisfactory workaround, which is to use

setup ‹Sign.mandatory_path "some_prefix"›

...

setup ‹Sign.parent_path›

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

Re: [isabelle-dev] LRZ outage

[Lars Hupel]

> I will update as soon as service resumes.

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

[isabelle-dev] LRZ outage

[Lars Hupel]

Dear developers,

it appears that there is a large-scale LRZ outage. The following 
services are affected:


- AFP submission service
- AFP slow tests

as well as other machines used privately by various people that are 
hosted in the Compute Cloud.


I will update as soon as service resumes.

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

Re: [isabelle-dev] Testing the QuickCheck setup

[Lars Hupel]

Hi Andreas,

thanks, you're making some good points.

> Testing quickcheck is indeed quite tricky. Do you know which of the
> quickcheck calls time out? Does it happen only with the random generator
> or also with exhaustive?

No, it fails on all of them.

> It might be that you have a fairly large set of code equations and the
> timeout already kicks in during code generation or compilation with
> PolyML, though. A larger timeout should help there.
> 
> Moreover, both statements have two free variables and you rely on the
> quickcheck generators being able to quickly come up with two different
> values for them. If you are not to set on the property, you could
> alternatively use
> 
> lemma "x ~= x" for x :: dec
> 
> which will definitely fail on the first generated example.

I'll apply both changes, in the hope that it makes it more robust.

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

[isabelle-dev] Testing the QuickCheck setup

[Lars Hupel]

Dear list,

I've been trying to test some QuickCheck generators in the CakeML
formalization, like so:



Unfortunately, it seems that they fail occasionally. I've tried
increasing the timeout, but that still seems to be problematic.

Is there a way to make these tests more robust? I don't want to comment
out the checks because much of the QuickCheck setup silently fails if
something is broken; meaning e.g. that Auto QuickCheck just doesn't work
on a proposition where it should work.

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

Re: [isabelle-dev] Problems connecting to https://isabelle.in.tum.de/repos/isabelle

[Lars Hupel]

In the past 2 days the isabelle_cronjob could not connect to
https://isabelle.in.tum.de/repos/isabelle -- but it appears to work 
from

most other hosts that I've tried. Maybe some odd change concerning SSL
certificates on the server vs. client side?


That's indeed strange. There was an issue with the machine lxbroy10, but 
as far as I could tell, it only affected SSH access. (The issue has been 
fixed by our ops this morning.)


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

Re: [isabelle-dev] Towards Isabelle2018-RC1

[Lars Hupel]

> I will produce Isabelle2018-RC1 later today, maybe in approx. 3h.
> 
> For that I also need a version of AFP that works.

According to , the latest
known-good version (except for the "slow" sessions) is

Isabelle/1b9462304e1d
AFP/2af750da996c
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Is hgbroy down?

[Lars Hupel]

> Apparently so. I'll let our administrators know.

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

Re: [isabelle-dev] Is hgbroy down?

[Lars Hupel]

> ~/isabelle/Repos/src/HOL: hg fetch
> remote: ssh: connect to host hgbroy.informatik.tu-muenchen.de port 22: 
> Operation timed out
> abort: no suitable response from remote hg!

Apparently so. I'll let our administrators know.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins reconfiguration

[Lars Hupel]

Does it mean that the great new hardware is now locked up and
exclusively available for Jenkins?


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

Re: [isabelle-dev] Jenkins reconfiguration

[Lars Hupel]

> - The "testboard" job will also be replaced to run Isabelle+AFP
> together. Historic builds will be deleted, as they are not relevant for
> the official history.

I have implemented this now. I'm currently monitoring the situation, but
so far, it seems like this sped up the process overall.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Jenkins reconfiguration

[Lars Hupel]

Dear Isabelle developers,

you may have already noticed that some Jenkins jobs got reconfigured.

The following changes are relevant for developers:

- The new job "isabelle-all" runs Isabelle+AFP together, incrementally.
This should improve overall performance and avoid double builds. There
is, once again, an automatic "grace period" of 2 minutes to allow
simultaneous Isabelle+AFP changes to be pushed before a build starts.


- The jobs "afp-repo" and "isabelle-repo" and subjobs will disappear
from the front page and the status page soon. Old links will continue to
work (i.e. historic builds will not be deleted).

- The "testboard" job will also be replaced to run Isabelle+AFP
together. Historic builds will be deleted, as they are not relevant for
the official history.

Some display changes:

Jenkins will show a failure summary on the link that is in the email
(example in the attachment).

There are more changes related to the testboard in the pipeline.

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

Re: [isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc

[Lars Hupel]

> I think it works properly now, see Isabelle/f0f83ce0badd + AFP/f7e9efc65d82.

Thanks for that. I'll proceed with the systems integration process of
that machine now.

> I usually measure the CPU time, multiply it by 2, and take the ceiling
> towards the next multiple of 300. In principle this maintenance of
> options could be automated.

The "multiple of 300" part is now implemented in "afp_check_roots"
(AFP/006f6826c3a1).

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

[isabelle-dev] LRZ outage

[Lars Hupel]

Dear users of the LRZ servers,

there appear to be some network and/or capacity problems at LRZ right
now, which is also why the "nightly" job failed just now. I hope this
will be resolved soon.

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

Re: [isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc

[Lars Hupel]

> But there are still (spurious) issues with some AFP sessions. With high
> contention (a total of 64 worker threads at the same time, e.g. with
> threads=2 and -j 32), some sessions will run into suspicious timeouts:
> 
> Timing Median_Of_Medians_Selection (2 threads, 25.039s elapsed time,
> 44.468s cpu time, 2.451s GC time, factor 1.78)
> *** Timeout
> Median_Of_Medians_Selection FAILED

Here are the offending sessions:

Dict_Construction
Hidden_Markov_Models
Median_Of_Medians_Selection
Mason_Stothers

They fail spuriously (except for the last one, which fails reproducibly)
when running with a total of 64 or even 128 worker threads:

./isabelle/bin/isabelle build -cbv -a -d afp-devel/thys/ -X slow -o
threads=2 -j 32

./isabelle/bin/isabelle build -cbv -a -d afp-devel/thys/ -X slow -o
threads=4 -j 32

None of this happens when using a total of just 32 worker threads.

Makarius, David, this probably requires another round of analysis.

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

Re: [isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc

[Lars Hupel]

>> So far it looks good, but we still need to test all of AFP.
> 
> I will do that today and report my findings.

The machine has been busy since yesterday running the distribution and
the AFP (except for slow) multiple times using different parameters.

The distribution is working fine.

But there are still (spurious) issues with some AFP sessions. With high
contention (a total of 64 worker threads at the same time, e.g. with
threads=2 and -j 32), some sessions will run into suspicious timeouts:

Timing Median_Of_Medians_Selection (2 threads, 25.039s elapsed time,
44.468s cpu time, 2.451s GC time, factor 1.78)
*** Timeout
Median_Of_Medians_Selection FAILED

The timeout for this session is 50 seconds. So I assume that this is
again a problem where the session itself runs through fine, but
something after that is not working well.

I'll send an update when I have more data points.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc

[Lars Hupel]

David has worked rather quickly and produced the following commit:
https://github.com/polyml/polyml/commit/86c52cbd8f6d

I have updated the polyml component accordingly in 
Isabelle/1b8457cc4de8.


So far it looks good, but we still need to test all of AFP.


I will do that today and report my findings.

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

[isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc

[Lars Hupel]

Dear list,

the good news is that we have just received new hardware (Dual Epyc 
7601).


The bad news is that a current development snapshot 
(Isabelle/410818a69ee3) exhibits a problem on this hardware. In 
particular, the session HOL-Corec_Examples doesn't appear to terminate.


$ cat .isabelle/etc/settings
init_components "$USER_HOME/.isabelle/contrib" 
"$ISABELLE_HOME/Admin/components/main"


ML_OPTIONS="-H 4000 --maxheap 8G"
ML_PLATFORM="$ISABELLE_PLATFORM64"

ML_HOME="$POLYML_HOME/$ML_PLATFORM"

ISABELLE_GHC=ghc
ISABELLE_POLYML="$ML_HOME/poly"
ISABELLE_SCALA="$SCALA_HOME/bin"
ISABELLE_OCAMLC=ocamlc
ISABELLE_OCAML=ocaml
ISABELLE_MLTON=mlton
ISABELLE_SWIPL=swipl
ISABELLE_SMLNJ=sml

The precise invocation is:

$ ./isabelle/bin/isabelle build -cbv -a -o threads=2 -j 16

Isabelle2017 "build -bva" works fine. This qualifies the problem as a 
regression, I suppose.


I've done some preliminary tracing; here are my findings:

- The "poly" process gets stuck at 100% CPU load and keeps calling 
"mmap"
- When trying to build the nonterminating session without "-b", it 
terminates
- GDB tells me the following stack trace when "mmap" is called (which 
corroborates that it happens during heap dumping):


#0  0x7f8dab80ba13 in __GI___mmap64 (addr=0x0, len=32768, prot=7, 
flags=34, fd=-1, offset=0) at ../sysdeps/unix/sysv/linux/mmap64.c:52
#1  0x00879d56 in OSMem::Allocate(unsigned long&, unsigned int) 
()
#2  0x00871c6e in MemMgr::NewExportSpace(unsigned long, bool, 
bool, bool) ()

#3  0x0085f020 in CopyScan::ScanAddressAt(PolyWord*) ()
#4  0x0088c2b6 in 
ScanAddress::ScanAddressesInObject(PolyObject*, unsigned long) ()

...
#24 0x0088c335 in 
ScanAddress::ScanAddressesInObject(PolyObject*, unsigned long) ()
#25 0x0088c8c1 in ScanAddress::ScanAddressesInRegion(PolyWord*, 
PolyWord*) ()

#26 0x008890a1 in SaveRequest::Perform() ()
#27 0x00882717 in Processes::BeginRootThread(PolyObject*) ()
#28 0x00874a9c in polymain ()
#29 0x7f8dab711b97 in __libc_start_main (main=0x405720 , 
argc=16, argv=0x7fffe693d4d8, init=, fini=out>, rtld_fini=, stack_end=0x7fffe693d4c8) at 
../csu/libc-start.c:310

#30 0x00405e01 in _start ()

I'm open to any suggestions for how to diagnose this. Happy to give out 
SSH access to the machine.


Cheers
Lars

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

Re: [isabelle-dev] quaternions

[Lars Hupel]

> So where does this material belong? Arguably not in Analysis, which is 
> already too large.

Why not a regular AFP entry?

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

[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

[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

[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

[isabelle-dev] ~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy broken

[Lars Hupel]

since approximately Isabelle/e0cd57aeb60c (~1 week):

*** Malformed global fact
"Misc_N2M.linorder_class.f1_t.n2m_t_ctor_fold_dict"
*** Illegal fixed variable: "s1"
*** At command "primrec" (line 164 of
"~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy")
___
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

[isabelle-dev] OCaml 4.06.0 drops nums.cma

[Lars Hupel]

I've been trying to figure out why some recent updates broke code
checking (both in the distribution and the AFP) for OCaml. It turns out
that the "nums.cma" module that we rely on for big integer arithmetic
got removed from the standard library.

This problem will affect anyone on rolling releases (e.g.
homebrew on macOS). Recent Ubuntu (18.04) does not appear to be affected.

The old module lives here now: 

To quote the README:

> This is a legacy library. It used to be part of the core OCaml
> distribution (in otherlibs/num) but is now distributed separately.
> New applications that need arbitrary-precision arithmetic should use
> the Zarith library (https://github.com/ocaml/Zarith) instead of the
> Num library, and older applications that already use Num are
> encouraged to switch to Zarith. Zarith delivers much better
> performance than Num and has a nicer API.

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

Re: [isabelle-dev] Cannot build HOL (again)

[Lars Hupel]

> Unknown JAVA_HOME -- Java unavailable

After removing .isabelle, you'll have to do the usual incantation to
retrieve the components:

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

[isabelle-dev] I/O error in isabelle build

[Lars Hupel]

I'm seeing some spurious (?) errors in "isabelle build":

17:15:13 Finished List-Index (0:00:08 elapsed time, 0:00:11 cpu time, 
factor 1.37)
17:15:13 *** I/O error: 
/tmp/isabelle-jenkins/process478460358635901180/export2631876 (No such 
file or directory)


I don't understand where these are coming from. One instance can be 
found here:


https://ci.isabelle.systems/jenkins/job/afp-repo-afp/1592/consoleFull

Of note are these warnings:

15:37:27 ### Ignoring bad database: 
"/media/data/jenkins/workspace/afp-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/Fishburn_Impossibility.db"
15:37:27 ### Ignoring bad database: 
"/media/data/jenkins/workspace/afp-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/FocusStreamsCaseStudies.db"
15:37:27 ### Ignoring bad database: 
"/media/data/jenkins/workspace/afp-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/HLDE.db"
15:37:27 ### Ignoring bad database: 
"/media/data/jenkins/workspace/afp-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/IEEE_Floating_Point.db"
15:37:27 ### Ignoring bad database: 
"/media/data/jenkins/workspace/afp-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/Program-Conflict-Analysis.db"
15:37:28 ### Ignoring bad database: 
"/media/data/jenkins/workspace/afp-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/Residuated_Lattices.db"
15:37:28 ### Ignoring bad database: 
"/media/data/jenkins/workspace/afp-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/Rewriting_Z.db"
15:37:28 ### Ignoring bad database: 
"/media/data/jenkins/workspace/afp-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/Shivers-CFA.db"


It also happened with the previous build on the same machine:

https://ci.isabelle.systems/jenkins/job/afp-repo-afp/1588/consoleFull

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

Re: [isabelle-dev] Possible non-determinism in HOL-ODE-Numerics

[Lars Hupel]

> Last known good state is:
> 
> Isabelle/7e349d1e3c95
> AFP/c3cfeceda7a0

We're back to normal now, as of

Isabelle/58c9231c2937
AFP/79f64c92d5ae
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Possible non-determinism in HOL-ODE-Numerics

[Lars Hupel]

(I meant "non-termination", of course, not "non-determinism".)

> Even if it'll terminate eventually (I'll keep it running for a bit
> longer), it surely is a sign of a performance degradation.

This run (threads=8) confirms that HOL-ODE-Numerics doesn't terminate
within 2 elapsed hours:

https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/754/consoleFull
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Possible non-determinism in HOL-ODE-Numerics

[Lars Hupel]

Isabelle/763f5a8f3f7f
AFP/2b0fc2365a6e

I'm unable to build the HOL-ODE-Numerics sessions. Usually, it takes 
about ~1 hour of CPU time (0:45 on lxcisa*).


It's been running for almost 2 CPU hours now on lxcisa0 (threads=10) and 
over 1:30 CPU hours on my i7 (threads=8). It also doesn't appear to 
terminate with threads=2. I'm unsure what's causing it.


Even if it'll terminate eventually (I'll keep it running for a bit 
longer), it surely is a sign of a performance degradation.


Last known good state is:

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

Re: [isabelle-dev] bad session structure

[Lars Hupel]

> I'm getting this message again. What gives? Everything is fully updated.
> 
> ~/isabelle/Repos/src/HOL: hg id
> 2e5b737810a6 tip

Do you have any uncommitted changes? Maybe in the AFP?

~/work/isabelle (default)$ isabelle-dev build -bva -D '$AFP'

works fine for me.

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

Re: [isabelle-dev] lxisabelle/lxcisa* maintenance

[Lars Hupel]

> Jenkins is back online. For technical reasons, lxcisa0 will only become
> available again tomorrow.

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

[isabelle-dev] Bad documentation directory

[Lars Hupel]

When I clone a fresh copy of Isabelle, or run "hg clean --all", then
"isabelle build" fails with the following error message:

*** Bad documentation directory:
"/home/lars/work/isabelle/src/Tools/jEdit/dist/doc"

That directory is not present by default and appears to be only created
by "isabelle jedit". A workaround is to always run "isabelle jedit -bf"
before running "isabelle build".
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] lxisabelle/lxcisa* maintenance

[Lars Hupel]

> - Jenkins
> - (shell access to) lxcisa0

Jenkins is back online. For technical reasons, lxcisa0 will only become
available again tomorrow.

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

[isabelle-dev] lxisabelle/lxcisa* maintenance

[Lars Hupel]

Dear users of lxisabelle/lxcisa*,

on Sunday, I will have to perform necessary maintenance. The following 
services may be interrupted and/or unavailable:


- Jenkins
- (shell access to) lxcisa0

In particular, I recommend to not start any new jobs on lxcisa0, as I 
might have to stop them. Please try to finish existing jobs by Sunday 
10am CET. Jenkins jobs will be disabled already on Saturday evening.


Regular operation continues on Monday.

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

Re: [isabelle-dev] NEWS: Latex errors

[Lars Hupel]

> * Command-line tool "isabelle document" has been re-implemented in
> Isabelle/Scala, with simplified arguments and explicit errors from the
> latex process. Minor INCOMPATIBILITY.

Featherweight_OCL now fails to build:

isabelle document -d
/home/lars/.isabelle/browser_info/AFP/Featherweight_OCL/outline -o pdf
-n outline -t -annexa\,afp\,/proof\,/ML
*** Latex error (line 183 of
"/home/lars/.isabelle/browser_info/AFP/Featherweight_OCL/annex-a/root.tex"):
***   LaTeX Error: No \title given.
*** Failed to build document in
"/home/lars/.isabelle/browser_info/AFP/Featherweight_OCL/annex-a"

I wonder if this error is genuine and just got swallowed before, or if
it's a side effect of the change.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Slow builds due to excessive heap images

[Lars Hupel]

> We are presently testing Poly/ML 5.7.1 by default (see
> Isabelle/aefaaef29c58) and there are already interesting performance
> figures, e.g. see:
> 
> http://isabelle.in.tum.de/devel/build_status
> http://isabelle.in.tum.de/devel/build_status/Linux_A
> http://isabelle.in.tum.de/devel/build_status/AFP
> 
> Overall, performance is mostly the same as in Poly/ML 5.6 from
> Isabelle2017, but there are some dropouts. In particular, loading heap
> images has become relatively slow: this impacts long heap chains like
> HOL-Analysis or big applications in AFP. E.g. see
> http://isabelle.in.tum.de/devel/build_status/AFP/index.html#session_CAVA_LTL_Modelchecker
> (timing vs. ML timing).

Tobias and me have discovered an interesting discrepancy between your
AFP slow setup and our AFP slow setup. They run on identical hardware
with the only difference of 6 vs 8 threads. On 6 threads, it runs
significantly faster. For example, Flyspeck-Tame requires 9:44:16
(elapsed time on 8 threads) vs 8:50:55 (elapsed time on 6 threads).

That difference aside, what I also find alarming is that the total
runtime of Flyspeck-Tame increased by more than 20% after the switch to
Poly/ML 5.7. This now means that the slow sessions rapidly approach 24
hours in build time, which makes it less feasible to run them every day.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] AFP statistics

[Lars Hupel]

> The devel equivalent is available at
>  and is re-generated every
> time someone pushes to the repository. Currently that one shows wrong
> dependency numbers because it hasn't been adapted yet to
> session-qualified imports. I'm still working on a proper fix.

The numbers on devel should now be correct again.

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

Re: [isabelle-dev] AFP statistics

[Lars Hupel]

> The AFP statistics https://www.isa-afp.org/statistics.html is very nice
> -- I often show the last diagram in presentations, as a proof of success
> of Isabelle as application platform over the years.
> 
> Who is actually responsible for this tool?

Me and our student Max Haslbeck. It is part of the site generator that
is invoked every time a new entry is added.

The devel equivalent is available at
 and is re-generated every
time someone pushes to the repository. Currently that one shows wrong
dependency numbers because it hasn't been adapted yet to
session-qualified imports. I'm still working on a proper fix.

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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Lars Hupel]

> My plan would be to fork the AFP 2017 release branch tomorrow (around 
> midnight CET from Mon to Tue).
> 
> There still seems to be quite a bit of ongoing activity - if there is 
> anything that needs to go into the afp-2017 release, please let me know.

One more thing that is of interest to users: the statistics page for
devel AFP is currently broken. I'm trying to fix this for the upcoming
2017 release.

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

Re: [isabelle-dev] isabelle build timing

[Lars Hupel]

> The canonical build parameters for this machine appear to be:
> 
>   isabelle build -j8 -o threads=6

I find this combination (8*6 = 48 threads) to be surprising, given that
that machine has only access to 22 physical (non-HT) cores. Judging from
your list below, this is the minimum number of threads you tried out
(for distribution only). Or am I reading the numbers wrong?
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice

[Lars Hupel]

Hi Viorel,

it's probably easiest to send a patch containing your changes to this mailing 
list. (Alternatively, a copy of all the files you changed.) Some Isabelle 
committer can then push this to the testboard which will run the whole AFP.

Cheers
Lars

On 27 August 2017 16:59:44 CEST, Viorel Preoteasa  
wrote:
>I managed to integrate the new complete distributive lattice into HOL 
>library.
>
>The changes are these:
>
>Complete_Lattice.thy
> - replaced the complete_distrib_lattice with the new stronger version.
>  - moved some proofs about complete_distrib_lattice and some 
>instantiations to Hilbert_Choice
>
>Hilbert_Choice.thy
> - added all results complete_distrib_lattice, including instantiations
>of set, fun that uses uses Hilbert choice.
>
>Enum.thy
>  - new proofs that finite_3 and finite_4 are complete_distrib_lattice.
>  - I added here the classes finite_lattice and finite_distrib_lattice
>and proved that they are complete. This simplified quite much the
>proofs
>that finite_3 and finite_4 are complete_distrib_lattice.
>
>Predicate.thy
>  - new proof that predicates are complete_distrib_lattice.
>
>I compiled HOL in Isabelle2017-RC0 using
>
>isabelle build -v -c HOL
>
>and I got:
>
>Timing HOL (2 threads, 266.231s elapsed time, 487.094s cpu time,
>43.344s 
>GC time, factor 1.83)
>Finished HOL (0:04:26 elapsed time)
>
>Finished at Sun Aug 27 17:41:30 GMT+3 2017
>0:04:37 elapsed time
>
>But I don't now how to go from here to have these changes into
>Isabelle.
>
>There is also AFP. If there are instantiations of 
>complete_distrib_lattice, then most probably they will fail.
>
>One simple solution in this case could be to keep also the
>old complete_distrib_lattice as complete_pseudo_distrib_lattice.
>
>Viorel
>
>
>On 8/26/2017 3:06 PM, Lawrence Paulson wrote:
>>> On 25 Aug 2017, at 20:14, Viorel Preoteasa
>>> > wrote:
>>>
>>> One possible solution:
>>>
>>> Add the new class in Complete_Lattice.thy, replacing the existing
>class
>>>
>>> Prove the instantiations and the complete_linearord subclass later
>>> in Hilbert_Choice.
>>>
>>> On the other hand, it seems inconvenient to have the Hilbert Choice
>>> to depend on so many other theories.
>> 
>> I’d prefer this provided the instantiations aren’t needed earlier.
>> 
>> The delay in the introduction of the Axiom of Choice is partly 
>> historical, but it’s worth noting how much of HOL can be developed 
>> without it.
>> 
>> Larry
>___
>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

[isabelle-dev] NEWS: Pattern Aliases

[Lars Hupel]

* Theory "HOL-Library.Pattern_Aliases" provides input and output syntax
for pattern aliases as known from Haskell, Scala and ML.


This is a small library theory providing convenient syntax for defining
recursive functions. Tobias is already using this for defining functions
over trees. For example:

function merge :: "('a::linorder) heap ⇒ 'a heap ⇒ 'a heap" where
"merge Leaf h = h" |
"merge h Leaf = h" |
"merge (Node l1 a1 r1 =: h1) (Node l2 a2 r2 =: h2) =
   (if a1 ≤ a2 then Node (merge h2 r1) a1 l1
else Node (merge h1 r2) a2 l2)"

Users of Haskell or Scala should be familiar with this syntax (both use
"@" instead of "=:", but "@" is already used in HOL).

To use this syntax, you need to import "HOL-Library.Pattern_Aliases" and
activate the bundle "pattern_aliases" either locally or globally. I
recommend doing this only locally, i.e.

context includes pattern_aliases begin

(* ... *)

end

This avoids polluting the global syntax.

Some more documentation can be found in the theory file.

There is still time to tweak this for the 2017 release, so comments are
welcome.

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

Re: [isabelle-dev] [158c513a39f5] JVM crash

[Lars Hupel]

> Lars, maybe you can run the same test on your machine and see what
> happens there.

I did, and nothing happened for about 100 iterations. I have a Core
i7-2600. OS is otherwise identical to Manuel (Arch Linux).

> As for Scala, could a problem in the Scala compiler really lead to the
> JVM segfaulting? I would have thought if the JVM segfaults, that's a bug
> in the JVM. (unless it's a hardware-related issue, of course)

I've seen it happening, but it is very rare. Still, the coincidence of
crashes during compilation could be explained by random chance (even if
very unlikely). A quick look over Scala's issue tracker reveals no
documented JVM segfaults after 2011.

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

Re: [isabelle-dev] [158c513a39f5] JVM crash

[Lars Hupel]

> on 158c513a39f5, I just had a JVM crash during "isabelle build" when it
> was building Isabelle/Scala. (Log attached).

I had a similar problem today. Unfortunately I didn't save the logfile.

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

Re: [isabelle-dev] Towards a "localized" code generator

[Lars Hupel]

Dear Andreas,

> Well, we here at ETH have another function transformer, which can also
> be activated and deactivated basically with almost the same pattern. The
> only difference is that at the moment we use a command rather than a
> Config value because de- and reactivation in our case has to do a bit
> more than just enabling/disabling a function transformer. It also must
> swap a few code equations.

Function transformers could also be declared with an attribute, although
there I'd say it's even less clear that attributes should be (ab)used
for that. Possibly instead we could have a command

functrans_setup "constructor_funs" = ‹
  (* implementation *)
›

... akin to simprocs. Of course, this would need to work in bundles as
well. (simprocs do work in bundles)

> This is an interesting idea. For the above-mentioned function
> transformer, we also have code_datatype declarations that must be
> switched back and forth. The big advantage of your approach seems to me
> that one can envision this alternative setup already where characters
> are defined (and similarly for int/nat/set/mapping/...).

Exactly, that's another goal that could be achieved.

> But I wonder
> whether these bundle targets can be extended later. That is, if is some
> unrelated theory, I write my own function for chars by pattern-matching
> on Char. If I then import your theory, can I add further declarations
> (code drop/code) to the bundle such that subsequent theories get a
> consistent setup no matter whether the unbundle the bundle or not?

Currently I'm unaware of any way to extend bundles, except for something
like:

bundle bar begin
  unbundle foo
end

Whether or not extending bundles is possible/canonical in Isar is a
question best answered by Makarius.

With locales, it would be possible, but of course they come with their
own sets of issues. The beauty of a localized tool is that it would work
uniformly across bundles and locales, so users can pick and choose.

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

[isabelle-dev] Towards a "localized" code generator

[Lars Hupel]

Dear users of the code generator,

last week I spoke with Florian about some fundamental properties of the
code generator.

Many Isabelle users are also "power users" of the code generator; in the
sense that they exploit many of its facilities (code printing, various
attributes, ...). These days the setup is really powerful and can be
tweaked in many ways.

However, only few bits of the code generator is actually localized: Off
the top of my head, this only applies to some of the attributes
("[code]" etc.). There are a lot of commands that only work in a global
context and have a permanent effect on the theory.

This has led to a problem: My work currently requires gathering code
equations for some constants. Afterwards, I need to prove some things
about them, which I do with either "code_simp" or "eval" – however, this
requires a different setup. To make matters worse, the gathering of the
code equations also requires special setup.

I'd like to share with you two strategies to cope with this situation.
This can serve as the basis for further discussion how to localize the
code generator.

1) Function transformers: I want to run a function transformer in
special situations. But I can only register it globally (with
"Code_Preproc.add_functrans"). What I use is the following pattern:

val enabled = Attrib.setup_config_bool @{binding "constructor_funs"} (K
false)

fun functrans ctxt thms = (* implementation *)

val code_functrans = Code_Preproc.simple_functrans (fn ctxt =>
  if Config.get ctxt enabled then
functrans ctxt
  else
K NONE)

I'm not sure whether this is how attributes are meant to be used, but at
least I can enable this locally. But as far as I can tell there are only
three function transformers in total, so I'm not sure how relevant this is.

2) "Fake local" declarations: I want to change the representation of the
"char" type in declared code. By default, it is represented using
numerals in a "non-free" way (i.e. there are invalid representations).
I'd like to replace it with a free representation (bytes), but don't
want this to affect the global theory; or at least, I'd like to avoid
people importing my theory to be affected [0].

Here's my workaround:

ML‹
  fun code_attribute f = Thm.declaration_attribute (fn thm =>
Context.mapping (f thm) I)
›

attribute_setup "code_datatype" = ‹
  Scan.repeat1 Args.term >> (fn terms =>
code_attribute (K (Code.declare_datatype_global (map dest_Const
terms
›

Now I can use the "bundle" target:


bundle char_byte_representation begin

declare [["code_datatype" char_of_byte]]

declare [[code drop: equal_char_inst.equal_char String.Char]]

(* more ... *)

declare char_byte_literals[code_unfold]

end

Importing this theory doesn't change the code setup. Only when I use
"unbundle" the changes become permanent. However, it doesn't work
properly in an unnamed context with "including" (this is as expected).
There are a lot of occurrences of "code_datatype", often leading to the
problem of artificially splitting up theories into an "abstract" and
"implementation" part.

Cheers
Lars



[0] This is not a theoretical problem, see AFP/e0065e482c76.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] map/rel/set for lift_bnf

[Lars Hupel]

> thanks for the reminder. Cf. c6714a9562ae and a5a24e1a6d6f.

Great, thanks!

> Note that this still doesn’t provide the interface to Lifting and Transfer 
> via transfer rules for the BNF constants (which is more complicated since 
> lift_bnf doesn’t know about Lifting, in particular about the correspondence 
> relations).

That's fair enough. The proofs are not that complicated.

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

Re: [isabelle-dev] The coming release of Isabelle2017

[Lars Hupel]

I currently supervise a student who's investigating proof refactoring. One 
possible outcome of this would be a tool that also does what you suggested. 
It's a little too early to tell, though.

Cheers
Lars

On 8 July 2017 23:28:42 CEST, Lawrence Paulson  wrote:
>No, that’s precisely what I’d like to avoid. I prefer texts that you
>can actually read. It would be great to have something automatically
>generated, even if it needed manual tweaking (e.g. to rename
>variables).
>
>And I’ve gone to some effort purging instances of “guess” from existing
>proofs.
>
>Larry
>
>> On 8 Jul 2017, at 22:16, Peter Lammich  wrote:
>> 
>> We already have proof goal_cases. Is that what you mean?
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] scala-2.12.2

[Lars Hupel]

> The patch is now running on testboard:
> .

Unfortunately, this patch did not work out.

22:13:39 *** Failed to finish proof (line 62 of
"~~/src/HOL/Library/Code_Target_Nat.thy"):
22:13:39 *** goal (1 subgoal):
22:13:39 ***  1. Transfer.Rel (rel_fun pcr_integer (rel_fun op = op =))
22:13:39 ***  (\a b. True) op =
22:13:39 *** At command "by" (line 62 of
"~~/src/HOL/Library/Code_Target_Nat.thy")
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] scala-2.12.2

[Lars Hupel]

> I took the opportunity to have a look at it and found out it can be done
> differently, see attached patch.

The patch is now running on testboard:
.

> The clue about "integer_of_char" is that it had to work regardless
> whether HOL chars are represented authentic or by target language
> characters (importing "~~/src/HOL/Library/Code_Char").
> 
> Nowadays this can be achieved without spelling out the chars explicitly.
>  The last stone to turn around before had been the de-constructivation
> of the char type (b3f2b8c906a6).

Thanks for investigating this.

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

Re: [isabelle-dev] scala-2.12.2

[Lars Hupel]

> The guys there are talking about Dotty. Do you think it will be also
> taken into account by the regular scalac maintainers eventually?

Those are Martin Odersky's students, so it's natural that they want to
avoid this in Dotty.

I'm confident that the scalac team at Lightbend will also have a look,
but we should give them a couple of days.

> Alternatively, if Florian has an idea for a workaround it is also fine.

I'm still not quite sure about the impact of this.

If I manually increase the stack size (-Xss), as is done in
ISABELLE_SCALAC_OPTIONS, the problem goes away (even for the full
"test.scala" file). This would explain why the problem didn't manifest
itself in the testboard. However, I'm not sure if we should expect users
of code generation to invoke compilers with specific options.

Regardless, this is clearly a regression in Scala.

Alternatively, Florian might offer some insight why he set up the code
equations for that particular constant in that way (see "String.thy",
where a ML snippet generates 256 code equations). Note that large
pattern matches on the JVM should be avoided, lest we violate the 64k
method length limit in class files ("integer_of_char" currently requires
58044 bytes).
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] scala-2.12.2

[Lars Hupel]

> a "StackOverflowError" (in the patmat phase), before I even got a chance
> at running this

I have investigated this now. It is a regression from Scala 2.11.x to
Scala 2.12.x.

The offending function is "integer_of_char", which performs a 256-way
pattern matching. Maybe this should be implemented differently.

In any case, I have filed this as a bug:

  

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

Re: [isabelle-dev] scala-2.12.2

[Lars Hupel]

> The scalac part should be OK. The problem is the scala part, i.e. actual
> runtime -- presumably the run_cmd here:
> http://isabelle.in.tum.de/repos/isabelle/annotate/20304512a33b/src/HOL/Library/code_test.ML#l562
> 
> I've just made a quick test of HOL-Codegenerator_Test on lxbroy10: it
> leads to a very long running java process. Killing that produces the
> following error:
> 
> *** Code check failed for Scala: isabelle_scala scalac
> $ISABELLE_SCALAC_OPTIONS ROOT.scala
> *** At command "export_code" (line 18 of
> "~~/src/HOL/Codegenerator_Test/Generate.thy")

Very curious, for multiple reasons:

- testboard is supposed to run Scala as well (I'll need to double check
that that's the case)
- the code check error message explicitly talks about "scalac"
- I just unpacked the attachment you sent and, with scalac 2.12.2 I get
a "StackOverflowError" (in the patmat phase), before I even got a chance
at running this
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] include option for "sessions" in ROOT

[Lars Hupel]

I'm playing around with the new "sessions" feature for qualified imports.

I think a prominent use case is to depend on various AFP entries. When
I'm working on my local development, I'd like to do this:

session Preliminiaries = ...
  sessions HOL-Library
  theories
HOL-Library.FSet ...
  sessions Coinductive
  theories
Coinductive ...

However, this only works when I have included the AFP, e.g. via "-d '$AFP'".

Why can I not specify this inline in the ROOT file? Like so:

session Preliminiaries = ...
  sessions HOL-Library
  theories
HOL-Library.FSet ...
  sessions Coinductive (from "$AFP")
  theories
Coinductive ...

That way, I don't have to remember to add the AFP in the command line.

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

Re: [isabelle-dev] scala-2.12.2

[Lars Hupel]

> I've just pushed the inverse patch of 94b0da1b242e to testboard, so
> we'll see.
> 
> 

HOL-Codegenerator_Test runs fine (0:14:41 elapsed time).

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

Re: [isabelle-dev] scala-2.12.2

[Lars Hupel]

> Maybe we should give it another try?

I've just pushed the inverse patch of 94b0da1b242e to testboard, so
we'll see.



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

Re: [isabelle-dev] Splitting of Iptables_Semantics_Examples

[Lars Hupel]

> The idea is to have a somewhat manageable chop from
> Iptables_Semantics_Examples within the range of a build with standard
> parameters (which means x86), merely guarded by "slow" group tag.
> 
> Thus it is visible in tests like "isabelle build -d '$AFP' -a -X
> very_slow" that I am doing manually all the time, e.g. when there is a
> change in the Poly/ML repository.
> 
> Since we did not have that for the huge Iptables_Semantics_Examples last
> year, we ran blindly into the unpleasant surprise of a Poly/ML 5.7
> version that no longer worked for us.

Ironically, this has now exhibited a problem in 5.6:

poly: scanaddrs.cpp:218: void
ScanAddress::ScanAddressesInRegion(PolyWord*, PolyWord*): Assertion
`obj->ContainsNormalLengthWord()' failed.

I have seen that once or twice before. I thought it was spurious, but
perhaps it should be investigated more.

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

[isabelle-dev] Splitting of Iptables_Semantics_Examples

[Lars Hupel]

Since AFP/b56d94d, the big session Iptables_Semantics_Examples is split
into four smaller sessions.

This poses a problem for the nightly job, which is running with -j1 and
threads=8. The parallelism in the four smaller sessions is much less
than the parallelism (factor 3) in the previous big session (factor 6).
This can be witnessed by the big jump in build time from build #441 to #442:




In fact, it takes longer than the hard-coded timeout of 20 hours for the
full job. Starting tomorrow, the build timeout will be 23.5 hours. (I'm
not sure whether or not that increase is sufficient.)

Still, this is somewhat unsatisfactory, because it means that the
maintenance window shrinks to some time between 2am and 3am CET.

There are two ways to avoid these excessive build times:

1) Backing out AFP/b56d94d.
2) Changing to -j2 with threads=4. This has the downside that there will
be a jump in measurements of JinjaThreads etc. Then again, I don't know
if anyone even looks at the statistics for isabelle-nightly-slow.

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

Re: [isabelle-dev] scala-2.12.2

[Lars Hupel]

> After your change d76937b773d9, I still see a non-terminating
> HOL-Codegenerator_Test. So in 94b0da1b242e I have switched back to
> scala-2.11.8.

Interesting. In Jenkins, this commit builds fine:
.
(I had tested it with testboard before anyway.)
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] scala-2.12.2

[Lars Hupel]

> With Isabelle/a43a079156a6 we are on scala-2.12.2, leaving the 2.11.x
> behind.

See also Isabelle/d76937b773d9, which repairs a broken code adaptation.
Note that `error` had been deprecated for at least one major release cycle.

Maybe we should start performing code checks with stricter compile flags
(e.g. "fatal warnings") to detect these problems early on.

Additionally, we might want to investigate checking multiple versions of
target languages. Three of the four platforms (Scala, Haskell, OCaml)
have tooling for selecting specific compiler versions available (sbt,
Stack, OPAM, respectively), whereas the fourth platform (SML) hardly, if
ever, makes breaking changes.

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

Re: [isabelle-dev] unable to start Isabelle/jEdit due to error in unused session

[Lars Hupel]

Dear Chris,

> 2) or there was some easy way (e.g., a flag) to exclude specific
> Isabelle components / sessions / ROOT files from checks (without having
> to edit "etc/settings").

I believe I have a solution for this problem.

For a while now, I've been using a custom Isabelle "launcher" based on
libisabelle [0]. It can be downloaded as a shell script [1]. It acts as
a wrapper for the regular Isabelle tool launcher. The twist is that it
supports on-the-fly registration of components.

In my setup, I've defined these two aliases:

alias isabelle='isabellectl --version 2016-1 --internal --afp --user
/home/lars exec'
alias isabelle-dev='isabellectl --devel --internal --component
/home/lars/work/afp --user /home/lars --home /home/lars/work/isabelle exec'

I can launch Isabelle by typing

$ isabelle jedit ...

or

$ isabelle-dev jedit ...

Note that additional arguments passed to the Isabelle tool need to be
separated by "--", as is standard practice in command-line environments:

$ isabelle-dev jedit -- -d . -l HOL-Library

But you can also pass in more components:

$ isabelle-dev --component /path/to/isafor jedit -- -l IsaFoR

Same thing works for using the stable version.

There are two caveats here:

- If you use the launcher for a stable Isabelle version, it'll download
a fresh copy to your home directory (Linux: "~/.local/share").
- The launcher claims control over your
"$ISABELLE_HOME_USER/etc/components" file. If you already have one, you
need to either delete it, or specify a different "--user" setting in the
alias.

This should work pretty much "out of the box" on Linux and OS X. No
guarantees on Windows.  You might also want to pass "--verbose" to get
informed about what is happening.

Cheers
Lars


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

Re: [isabelle-dev] Uses of Jenkins at TUM

[Lars Hupel]

>   * My main use of Mira was to figure out which Isabelle version
> corresponds to which AFP version, when something was broken in AFP.
> 
>   * I did not find this information in Jenkins, when I was still
> spending more time on it last year.

This information is all there. Build status is accessible via the
Jenkins API, of which you are undoubtedly aware. We also had both public
and private conversations where I pointed out to you where this is
available.

The user-facing side of this is
, which broke sometime around
Isabelle/7ca8810b1d48 though no change of my own, but so far I haven't
had time to investigate what caused it. (All entries are marked as
"skipped".)

>   * For actual quasi-interactive testing I always use "isabelle build"
> directly on a local or remote machine, with incrementally updated global
> build state (heaps and logs). Here it is important to get results within
> approx. 20-30 min -- presently we are at > 30 min.

This has also already been discussed. The vast majority of people I
asked is interested in quick feedback about AFP, which the testboard
provides.

> When Jenkins was about to supersede isatest last year, I put forward
> missing requirements e.g. here:
> http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg06783.html

This has also already been discussed. Testing with x86 caused too many
spurious failures, even after countless hours of tweaking parameters. I
refuse to take flak for reducing build noise.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Uses of Jenkins at TUM

[Lars Hupel]

> In parallel (before and after Mira) we've had the older isatest. I don't
> know if Mira ever had the ambition to replace isatest, but Jenkins tried
> to do all that and failed. This was the start of my great worries about
> the Isabelle administration and release infrastructure ...

So, you're just going to unilaterally declare that it all failed and we
should take your word for that?

The cliché that "Jenkins did X" is getting a bit old. At least be honest
and say my name, because it is me who built up that infrastructure. (Not
without external input, constraints, and requirements, but still.)

Finally, let me make one thing very clear: I strongly object to this
passive-aggressive attitude (not just about Jenkins, even). I have
little interest in arguing if there's not even a trace of mutual
understanding and charity.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Bad theory import "Main"

[Lars Hupel]

> This is still "blame game".

If you say so.

> I actually offered an open dialog about it last December, and you
> rejected that.

Because the offer consisted merely of rehashing things we already talked
about in person. To be completely frank, I'm tired of repeating myself
and others endlessly.

For the record, the lxcisa0 host is the result of a compromise that both
Jenkins and what you asked for (a publicly-accessible beefy machine)
should be accommodated for. I wouldn't call that rejection.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev