Does it terminate?

[clarus]

I have a question. It seems to me that this package takes a really long time to compile. I tested the v8.6.0 release and:

• on my machine I get a segfault because of memory exhaustion I guess;
• on the server for the opam bench it gets a timeout after 5 hours https://coq-bench.github.io/clean/Linux-x86_64-4.05.0-2.0.1/released/8.6.1/intuitionistic-nuprl/8.6.0.html :

...
- coqc -Q close "" stronger_continuity_rule3.v
- coqc -Q close "" stronger_continuity_rule4.v
- coqc -Q close "" stronger_continuity_rule4_v2.v
- coqc -Q close "" stronger_continuity_rule4_v3.v
- coqc -Q close "" stronger_continuity_rule4_v2_2.v
- coqc -Q close "" continuity_stuff.v
[timeout]

Is it just me or this package is extremely slow? Does it terminate? The next question being: at which point being slow is considered as a bug and should we continue to distribute an opam package for it?

[clarus]

Did anyone have time to look at this issue? I am about to remove the opam package of intuitionistic-nuprl as this is unclear if its compilation terminates.

[Zimmi48]

I remember this package to be known as taking a very long time to terminate: on Jenkins @MatejKosik had created a bench with it and a bench without. @herbelin or any of the experienced developers know about this package and should be able to comment further.

[clarus]

OK thanks.

[clarus]

For information, I added this package to a black list for https://coq-bench.github.io/

[palmskog]

@clarus this project is maintained upstream, so this repo could be considered obsolete: https://github.com/vrahli/NuprlInCoq

I think we can keep the packages for historical preservation purposes.

[Zimmi48]

See also coq-community/manifesto#60 (comment). I proposed to archive the coq-contrib copy of the repository, but didn't get any answer.