[isabelle] Cannot build HOL.Complex_Main · Mirror: Isabelle Users Mailing List

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Cannot build HOL.Complex_Main

Email Gateway (May 17 2021 at 10:07):

From: Yann Leray <yann.leray@inria.fr>
Hello,
I am working on Isabelle/Dedukti, a module to output Isabelle proofs in
Dedukti and Lambdapi.
In this context, I want to build the standard library, and I need Pure
as the basis (I think this is important for my problem).
However, the build won't finish for various reasons. (I got 2 different
reasons for 2 tries which I linked).
Can you explain what I may be doing wrong?

I am new to Isabelle and not well acquainted to even the build
mechanism, as I had for a long time good enough sessions/config files,
so I may probably have missed an important setting or done something
blatantly problematic.

Thanks for your time,

Yann Leray

NB: The machine where I'm running this has 64GB of RAM and about 5GB of
free disk space
NB: I'm not exactly running "isabelle build All" but the module
Dedukti_Import calls for a build, and I am convinced this is where my
problem lies

Relevant session definition:

session All in "Ex/All" = Pure +
options [export_theory, export_proofs, record_proofs = 2]
sessions HOL
theories
HOL.Complex_Main

Standard output:

Started at Thu May 6 01:36:02 GMT 2021

Build started for Isabelle/All ...
Running All ...
All: theory Tools.Code_Generator
All: theory HOL.HOL
All: theory HOL.Argo
All: theory HOL.SAT
[cut ...]
All: theory HOL.Presburger
All: theory HOL.Sledgehammer
All: theory HOL.List
All: theory HOL.Groups_List
All: theory HOL.Factorial
All: theory HOL.Binomial
All: theory HOL.GCD
All: theory HOL.Map
All: theory HOL.Enum
Run out of store - interrupting threads
All FAILED
(see also
/home/ubuntu/.isabelle/Isabelle2021/heaps/polyml-5.8.2_x86_64_32-linux/log/All)

*** exception Fail raised (line 2220 of "proofterm.ML"): Interrupt:
potential resource problems while exporting proof 2562160
*** At command "by" (line 933 of "~~/src/HOL/Enum.thy")
Unfinished session(s): All

Finished at Thu May 6 02:56:39 GMT 2021
1:20:37 elapsed time

Standard error:

*** Failed to build Isabelle/All

Standard output 2:

Started at Thu May 6 15:36:00 GMT 2021

Standard error 2:

Exception in thread "Isabelle.message_output"
java.lang.IndexOutOfBoundsException: Range [0, 0 + -194519867) out of
bounds for length 65536
        at
java.base/jdk.internal.util.Preconditions.outOfBounds(Preconditions.java:64)
        at
java.base/jdk.internal.util.Preconditions.outOfBoundsCheckFromIndexSize(Preconditions.java:82)
        at
java.base/jdk.internal.util.Preconditions.checkFromIndexSize(Preconditions.java:343)
        at
java.base/java.util.Objects.checkFromIndexSize(Objects.java:411)
        at java.base/sun.nio.ch.NioSocketImpl.read(NioSocketImpl.java:339)
        at
java.base/sun.nio.ch.NioSocketImpl$1.read(NioSocketImpl.java:803)
        at
java.base/java.net.Socket$SocketInputStream.read(Socket.java:981)
        at isabelle.Prover.read_chunk_bytes$1(prover.scala:290)
        at isabelle.Prover.$anonfun$message_output$1(prover.scala:316)
        at
isabelle.Isabelle_Thread$.$anonfun$fork$2(isabelle_thread.scala:65)
        at isabelle.Isabelle_Thread.run(isabelle_thread.scala:141)

Email Gateway (May 20 2021 at 11:26):

From: Makarius <makarius@sketis.net>
On 17/05/2021 06:25, Yann Leray wrote:

I am working on Isabelle/Dedukti, a module to output Isabelle proofs in
Dedukti and Lambdapi.

However, the build won't finish for various reasons.

NB: The machine where I'm running this has 64GB of RAM and about 5GB of free
disk space
NB: I'm not exactly running "isabelle build All" but the module Dedukti_Import
calls for a build, and I am convinced this is where my problem lies

Relevant session definition:

session All in "Ex/All" = Pure +
options [export_theory, export_proofs, record_proofs = 2]
sessions HOL
theories
HOL.Complex_Main

Standard output:

Started at Thu May 6 01:36:02 GMT 2021

Build started for Isabelle/All ...
Running All ...
All: theory Tools.Code_Generator
All: theory HOL.HOL
All: theory HOL.Argo
All: theory HOL.SAT
[cut ...]
All: theory HOL.Presburger
All: theory HOL.Sledgehammer
All: theory HOL.List
All: theory HOL.Groups_List
All: theory HOL.Factorial
All: theory HOL.Binomial
All: theory HOL.GCD
All: theory HOL.Map
All: theory HOL.Enum
Run out of store - interrupting threads
All FAILED
(see also
/home/ubuntu/.isabelle/Isabelle2021/heaps/polyml-5.8.2_x86_64_32-linux/log/All)
*** exception Fail raised (line 2220 of "proofterm.ML"): Interrupt: potential
resource problems while exporting proof 2562160
*** At command "by" (line 933 of "~~/src/HOL/Enum.thy")
Unfinished session(s): All

This looks fine so far. The export_proofs option is the result of some
explorative work that I did with Michael Färber approx. 1 year ago, and we
managed to get exactly to HOL.Enum: it requires careful inspection how these
proofs are done internally to get beyond that stage.

Afterwards, additional stages of exploration will be required to export all of
Main or even Complex_Main eventually.

Exception in thread "Isabelle.message_output"
java.lang.IndexOutOfBoundsException: Range [0, 0 + -194519867) out of bounds
for length 65536
        at
java.base/jdk.internal.util.Preconditions.outOfBounds(Preconditions.java:64)
        at
java.base/jdk.internal.util.Preconditions.outOfBoundsCheckFromIndexSize(Preconditions.java:82)

at
java.base/jdk.internal.util.Preconditions.checkFromIndexSize(Preconditions.java:343)

at java.base/java.util.Objects.checkFromIndexSize(Objects.java:411)
        at java.base/sun.nio.ch.NioSocketImpl.read(NioSocketImpl.java:339)
        at java.base/sun.nio.ch.NioSocketImpl$1.read(NioSocketImpl.java:803)
        at java.base/java.net.Socket$SocketInputStream.read(Socket.java:981)
        at isabelle.Prover.read_chunk_bytes$1(prover.scala:290)
        at isabelle.Prover.$anonfun$message_output$1(prover.scala:316)
        at isabelle.Isabelle_Thread$.$anonfun$fork$2(isabelle_thread.scala:65)
        at isabelle.Isabelle_Thread.run(isabelle_thread.scala:141)

That is a Java crash, which I have not yet seen before. Maybe it is a
consequence of recent renovations of the underlying socket implementation.

The negative integer looks suspiciously like an overflow of the machine word
type that is historically called "int".

Anyway, I think we should have a private discussion (including Frederic
Blanqui) about the current status of this unfinished research and development
from last year.

I am presently lagging behind many weeks in my mail folder, but this is
sufficiently important to move forward soon.

Makarius

Last updated: Jul 15 2022 at 23:21 UTC