From 5fd6e981be7d45c1b25b4bcc80c6e099fcfa0536 Mon Sep 17 00:00:00 2001 From: carte731 Date: Thu, 29 May 2025 07:01:55 -0700 Subject: [PATCH 01/10] Removed 'GeneralizedNewtypeDeriving' unused pragma from 'what4.hs' in Copilot-Theorem. --- copilot-theorem/src/Copilot/Theorem/What4.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/copilot-theorem/src/Copilot/Theorem/What4.hs b/copilot-theorem/src/Copilot/Theorem/What4.hs index 818ac9b3a..a6f0cf57a 100644 --- a/copilot-theorem/src/Copilot/Theorem/What4.hs +++ b/copilot-theorem/src/Copilot/Theorem/What4.hs @@ -1,7 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiWayIf #-} From b3e6110c238be5460a6ea0b005a3f053a2b212ab Mon Sep 17 00:00:00 2001 From: carte731 Date: Thu, 29 May 2025 07:04:04 -0700 Subject: [PATCH 02/10] Removed 'MultiWayIf' unused pragma from 'what4.hs' in Copilot-Theorem. --- copilot-theorem/src/Copilot/Theorem/What4.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/copilot-theorem/src/Copilot/Theorem/What4.hs b/copilot-theorem/src/Copilot/Theorem/What4.hs index a6f0cf57a..2203b35df 100644 --- a/copilot-theorem/src/Copilot/Theorem/What4.hs +++ b/copilot-theorem/src/Copilot/Theorem/What4.hs @@ -3,7 +3,6 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE LambdaCase #-} -{-# LANGUAGE MultiWayIf #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} From 3a66b167e702da01cb9965a1451be4d36331e7d2 Mon Sep 17 00:00:00 2001 From: carte731 Date: Thu, 29 May 2025 07:05:14 -0700 Subject: [PATCH 03/10] Removed 'StandaloneDeriving' unused pragma from 'what4.hs' in Copilot-Theorem. --- copilot-theorem/src/Copilot/Theorem/What4.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/copilot-theorem/src/Copilot/Theorem/What4.hs b/copilot-theorem/src/Copilot/Theorem/What4.hs index 2203b35df..4395a7b15 100644 --- a/copilot-theorem/src/Copilot/Theorem/What4.hs +++ b/copilot-theorem/src/Copilot/Theorem/What4.hs @@ -6,7 +6,6 @@ {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeApplications #-} From 55b8d2a0c79f370cedf0e9cb38c788cb4d4c0cdd Mon Sep 17 00:00:00 2001 From: carte731 Date: Thu, 29 May 2025 07:07:14 -0700 Subject: [PATCH 04/10] Removed 'TemplateHaskell' unused pragma from 'what4.hs' in Copilot-Theorem. --- copilot-theorem/src/Copilot/Theorem/What4.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/copilot-theorem/src/Copilot/Theorem/What4.hs b/copilot-theorem/src/Copilot/Theorem/What4.hs index 4395a7b15..2f60ee257 100644 --- a/copilot-theorem/src/Copilot/Theorem/What4.hs +++ b/copilot-theorem/src/Copilot/Theorem/What4.hs @@ -6,7 +6,6 @@ {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} From 697b43e60e849ba106069e228eb403df8c1d3a97 Mon Sep 17 00:00:00 2001 From: carte731 Date: Thu, 29 May 2025 07:08:44 -0700 Subject: [PATCH 05/10] Removed 'TupleSections' unused pragma from 'what4.hs' in Copilot-Theorem. --- copilot-theorem/src/Copilot/Theorem/What4.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/copilot-theorem/src/Copilot/Theorem/What4.hs b/copilot-theorem/src/Copilot/Theorem/What4.hs index 2f60ee257..4c9d62af8 100644 --- a/copilot-theorem/src/Copilot/Theorem/What4.hs +++ b/copilot-theorem/src/Copilot/Theorem/What4.hs @@ -6,7 +6,6 @@ {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} From 18a02dca20e338bb263f046367ff8b6b290a2b12 Mon Sep 17 00:00:00 2001 From: carte731 Date: Thu, 29 May 2025 07:10:00 -0700 Subject: [PATCH 06/10] Removed 'LambdaCase' unused pragma from 'Prover.hs' in Copilot-Theorem. --- copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs index 66db2c346..4bb52322e 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE LambdaCase #-} {-# LANGUAGE Trustworthy #-} -- | A prover backend based on Kind2. From 475bd6198201d875745ef1c62c1d83ab0005dc0b Mon Sep 17 00:00:00 2001 From: carte731 Date: Thu, 29 May 2025 07:11:08 -0700 Subject: [PATCH 07/10] Removed 'LambdaCase' unused pragma from 'SMTIO.hs' in Copilot-Theorem. --- copilot-theorem/src/Copilot/Theorem/Prover/SMTIO.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/copilot-theorem/src/Copilot/Theorem/Prover/SMTIO.hs b/copilot-theorem/src/Copilot/Theorem/Prover/SMTIO.hs index 2ce606b31..3035f718e 100644 --- a/copilot-theorem/src/Copilot/Theorem/Prover/SMTIO.hs +++ b/copilot-theorem/src/Copilot/Theorem/Prover/SMTIO.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE LambdaCase #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE Safe #-} From 5a587c2ea934a153b1e8876c5f2e43b4e540c39c Mon Sep 17 00:00:00 2001 From: carte731 Date: Thu, 29 May 2025 09:24:36 -0700 Subject: [PATCH 08/10] Updated CHANGELOG for Copilot-Theorem. --- copilot-theorem/CHANGELOG | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index f221aec44..29b457326 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,3 +1,12 @@ +2025-05-29 + * Version bump (4.4.1). (#613) + * Removed unused pragma: GeneralizedNewtypeDeriving from 'What4.hs' (#613) + * Removed unused pragma: MultiWayIf from 'What4.hs' (#613) + * Removed unused pragma: StandaloneDeriving from 'What4.hs' (#613) + * Removed unused pragma: TemplateHaskell from 'What4.hs' (#613) + * Removed unused pragma: TupleSections from 'What4.hs' (#613) + * Removed unused pragma: LambdaCase from 'Prover.hs' (#613) + * Removed unused pragma: LambdaCase from 'SMTIO.hs' (#613) 2025-05-07 * Version bump (4.4). (#618) * Translate quantifiers correctly in Kind2 backend. (#594) From 6a461f65eae6bdd5337ea08d00d28d13ebbcfbff Mon Sep 17 00:00:00 2001 From: carte731 Date: Wed, 25 Jun 2025 05:43:50 -0700 Subject: [PATCH 09/10] Updated and fixed the change log. --- copilot-theorem/CHANGELOG | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index 29b457326..a5edc99aa 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,12 +1,6 @@ 2025-05-29 - * Version bump (4.4.1). (#613) - * Removed unused pragma: GeneralizedNewtypeDeriving from 'What4.hs' (#613) - * Removed unused pragma: MultiWayIf from 'What4.hs' (#613) - * Removed unused pragma: StandaloneDeriving from 'What4.hs' (#613) - * Removed unused pragma: TemplateHaskell from 'What4.hs' (#613) - * Removed unused pragma: TupleSections from 'What4.hs' (#613) - * Removed unused pragma: LambdaCase from 'Prover.hs' (#613) - * Removed unused pragma: LambdaCase from 'SMTIO.hs' (#613) + * Removed unused pragma. (#613) + 2025-05-07 * Version bump (4.4). (#618) * Translate quantifiers correctly in Kind2 backend. (#594) From 317d34d82341c34e6ce21efead8628d2af17babb Mon Sep 17 00:00:00 2001 From: carte731 Date: Wed, 25 Jun 2025 05:44:22 -0700 Subject: [PATCH 10/10] Forgot the 's' on pragma. --- copilot-theorem/CHANGELOG | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index a5edc99aa..d28cc3041 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,5 +1,5 @@ 2025-05-29 - * Removed unused pragma. (#613) + * Removed unused pragmas. (#613) 2025-05-07 * Version bump (4.4). (#618)