Page MenuHomeIsabelle/Phabricator

HOL-Quickcheck_Examples fails on Windows
Open, LowPublic

Description

HOL-Quickcheck_Examples fails on Windows as follows:

*** quickcheck expected to find a counterexample but did not find one
*** At command "quickcheck" (line 72 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy")
*** quickcheck expected to find a counterexample but did not find one
*** At command "quickcheck" (line 68 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy")
*** quickcheck expected to find a counterexample but did not find one
*** At command "quickcheck" (line 62 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy")
*** quickcheck expected to find a counterexample but did not find one
*** At command "quickcheck" (line 56 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy")
*** quickcheck expected to find a counterexample but did not find one
*** At command "quickcheck" (line 40 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy")
*** quickcheck expected to find a counterexample but did not find one
*** At command "quickcheck" (line 30 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy")

This refers e.g. to current Isabelle/b3b992f6ad8f, but the problem has been there for several years.

Event Timeline

makarius triaged this task as Low priority.Jan 16 2020, 4:07 PM
makarius created this task.