[isabelle-dev] Resource problems with HOL-Quickcheck_Benchmark

[Makarius]

Dear experts on quickcheck and find_unused_assms,

we've seen resource problems with HOL-Quickcheck_Benchmark since the
introduction of polyml-5.8 in Isabelle/63721ee8c86c.


After several rounds of looking through the examples and the
implementation, and after some private discussions with David Matthews,
I have managed to recover the test as follows:

changeset:   70119:b48a496ca0cd
tag:         tip
user:        wenzelm
date:        Thu Apr 11 12:41:50 2019 +0200
files:
src/Benchmarks/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy
description:
more robust test: avoid spurious Interrupt (stack overflow?) due to
List.fun_lub_parametric;

diff -r 62b875ba33e1 -r b48a496ca0cd
src/Benchmarks/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy
--- a/src/Benchmarks/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy
Thu Apr 11 12:38:22 2019 +0200
+++ b/src/Benchmarks/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy
Thu Apr 11 12:41:50 2019 +0200
@@ -27,7 +27,10 @@

 context notes [[quickcheck_finite_types = true]]
 begin
-  find_unused_assms List
+  context notes [[quickcheck_finite_type_size = 2]]
+  begin
+    find_unused_assms List
+  end
   find_unused_assms Map
 end


The problem is only a single theorem: List.fun_lub_parametric -- see
also the attached Scratch.thy -- it occurs on reasonably fast machines
(e.g. macbroy2, lxcisa0).

Instead of default x86_64_32, I have also tried full x86_64: here the
same problem occurs at a total ML process size beyond 11 GB.

Could there be a situation where the "exhaustive" tester produces really
large lists (millions of entries) and then runs in stack-overflow due to
the recursive Generated_Code.map function?


	Makarius
-------------- next part --------------
theory Scratch
  imports Main
begin

declare [[quickcheck_finite_types, quickcheck_finite_type_size = 2]]  (* 2: OK, 3: Interrupt *)
ML \<open>Find_Unused_Assms.check_unused_assms \<^context> ("test", @{thm List.fun_lub_parametric})\<close>

end