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

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

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)

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 liesRelevant session definition:

session All in "Ex/All" = Pure +

options [export_theory, export_proofs, record_proofs = 2]

sessions HOL

theories

HOL.Complex_MainStandard 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: Dec 08 2021 at 09:20 UTC