From 6d21db68dd978669bfd4af53cc1b319be4955d78 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 16 Jul 2026 23:09:28 +0000 Subject: [PATCH] qc: rename QuickChick Derive commands to QCDerive QuickChick renamed its Derive vernacular to QCDerive (QuickChick's 24284a9 "Add QCDerive to disambiguate from Derive from other plugins", with the old command since removed), so the qc volume no longer compiles against coq-quickchick dev. Rename the ten command occurrences; requires a QuickChick with QCDerive (dev). Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw --- qc-current/QC.v | 4 ++-- qc-current/QuickChickTool.v | 2 +- qc-current/TImp.v | 14 +++++++------- 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/qc-current/QC.v b/qc-current/QC.v index 9dd674bad..877117487 100644 --- a/qc-current/QC.v +++ b/qc-current/QC.v @@ -1289,7 +1289,7 @@ End DefineGenSized. [QuickChick] provides some automation for deriving such instances for simple datatypes automatically! *) -Derive Arbitrary for Tree. +QCDerive Arbitrary for Tree. (** ===> GenSizedree is defined @@ -1298,7 +1298,7 @@ Derive Arbitrary for Tree. Print GenSizedTree. Print ShrinkTree. -Derive Show for Tree. +QCDerive Show for Tree. (** ===> ShowTree is defined *) diff --git a/qc-current/QuickChickTool.v b/qc-current/QuickChickTool.v index 8a4d4bc7d..8f2b23fcd 100644 --- a/qc-current/QuickChickTool.v +++ b/qc-current/QuickChickTool.v @@ -126,7 +126,7 @@ Inductive exp : Type := (** Since [exp] is a simple datatype, QuickChick can derive a generator, a shrinker, and a printer automatically. *) -Derive (Arbitrary, Show) for exp. +QCDerive (Arbitrary, Show) for exp. (** The [eval] function evaluates an expression to a number. *) Fixpoint eval (e : exp) : nat := diff --git a/qc-current/TImp.v b/qc-current/TImp.v index 780fc3975..7bc2d5d25 100644 --- a/qc-current/TImp.v +++ b/qc-current/TImp.v @@ -136,7 +136,7 @@ Inductive ty := TBool | TNat. QuickChick provides a top-level vernacular command to derive such instances. *) -Derive (Arbitrary, Show) for ty. +QCDerive (Arbitrary, Show) for ty. (* ==> GenSizedty is defined Shrinkty is defined @@ -352,7 +352,7 @@ Inductive exp : Type := (** To print expressions we derive a [Show] Instance. *) -Derive Show for exp. +QCDerive Show for exp. (* ================================================================= *) (** ** Typed Expressions *) @@ -699,7 +699,7 @@ Definition gen_typed_has_type := Inductive value := VNat : nat -> value | VBool : bool -> value. -Derive Show for value. +QCDerive Show for value. (** We can also quickly define a typing relation for values, a Dec instance for it, and a generator for values of a given type. *) @@ -862,7 +862,7 @@ Definition expression_soundness_exec := (** Let's see what happens if we use the default shrinker for expressions carelessly. *) -Derive Shrink for exp. +QCDerive Shrink for exp. Definition expression_soundness_exec_firstshrink := let num_vars := 4 in @@ -1088,7 +1088,7 @@ Notation "'WHILE' b 'DO' c 'END'" := Notation "'TEST' c1 'THEN' c2 'ELSE' c3 'FI'" := (CIf c1 c2 c3) (at level 80, right associativity). -Derive Show for com. +QCDerive Show for com. (** (Of course, the derived [Show] instance is not going to use these notations!) *) @@ -1296,7 +1296,7 @@ Conjecture well_typed_state_never_stuck : produce such generators -- i.e., generators for data structures satisfying inductively defined properties! *) -Derive ArbitrarySizedSuchThat for (fun v => has_type_value v T). +QCDerive ArbitrarySizedSuchThat for (fun v => has_type_value v T). (** ===> GenSizedSuchThathas_type_value is defined. *) @@ -1345,7 +1345,7 @@ Print GenSizedSuchThathas_type_value. (** Moreover, QuickChick can also derive DecOpt instances automatically, as well as proofs of correctness! *) -Derive DecOpt for (has_type_value v T). +QCDerive DecOpt for (has_type_value v T). Print DecOpthas_type_value.