From 282a78fe127040aa77d042b01fa21b868e8dc7e4 Mon Sep 17 00:00:00 2001 From: carte731 Date: Thu, 29 May 2025 07:01:55 -0700 Subject: [PATCH 1/8] copilot-theorem: Remove 'GeneralizedNewtypeDeriving' unused pragma from 'what4.hs'. Refs #613. The code of copilot-theorem contains unused language pragmas. To comply with our coding style, which required unused code not to be included in the codebase, those pragmas should be removed. This commit removes an unused pragma from Copilot.Theorem.What4. --- copilot-theorem/src/Copilot/Theorem/What4.hs | 29 ++++++++++---------- 1 file changed, 14 insertions(+), 15 deletions(-) diff --git a/copilot-theorem/src/Copilot/Theorem/What4.hs b/copilot-theorem/src/Copilot/Theorem/What4.hs index 818ac9b3a..c2c7eb01b 100644 --- a/copilot-theorem/src/Copilot/Theorem/What4.hs +++ b/copilot-theorem/src/Copilot/Theorem/What4.hs @@ -1,18 +1,17 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE MultiWayIf #-} -{-# LANGUAGE PatternSynonyms #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TupleSections #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} -- | -- Module : Copilot.Theorem.What4 From ad38ba44ee3e45ce0a196e5f4e78d981b3943236 Mon Sep 17 00:00:00 2001 From: carte731 Date: Thu, 29 May 2025 07:04:04 -0700 Subject: [PATCH 2/8] copilot-theorem: Remove 'MultiWayIf' unused pragma from 'what4.hs'. Refs #613. The code of copilot-theorem contains unused language pragmas. To comply with our coding style, which required unused code not to be included in the codebase, those pragmas should be removed. This commit removes an unused pragma from Copilot.Theorem.What4. --- 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 c2c7eb01b..7c7e84233 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 4f5f09adc31500cfd30950d31de3d7a6d4180f76 Mon Sep 17 00:00:00 2001 From: carte731 Date: Thu, 29 May 2025 07:05:14 -0700 Subject: [PATCH 3/8] copilot-theorem: Remove 'StandaloneDeriving' unused pragma from 'what4.hs'. Refs #613. The code of copilot-theorem contains unused language pragmas. To comply with our coding style, which required unused code not to be included in the codebase, those pragmas should be removed. This commit removes an unused pragma from Copilot.Theorem.What4. --- 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 7c7e84233..8610571c0 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 61fa0b46cfd7fec8964b328fc9625243e6fa412e Mon Sep 17 00:00:00 2001 From: carte731 Date: Thu, 29 May 2025 07:07:14 -0700 Subject: [PATCH 4/8] copilot-theorem: Remove 'TemplateHaskell' unused pragma from 'what4.hs'. Refs #613. The code of copilot-theorem contains unused language pragmas. To comply with our coding style, which required unused code not to be included in the codebase, those pragmas should be removed. This commit removes an unused pragma from Copilot.Theorem.What4. --- 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 8610571c0..c9da7fe8b 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 3088023b5e781b65afb8f4c96d93085c4a17b7fd Mon Sep 17 00:00:00 2001 From: carte731 Date: Thu, 29 May 2025 07:08:44 -0700 Subject: [PATCH 5/8] copilot-theorem: Remove 'TupleSections' unused pragma from 'what4.hs'. Refs #613. The code of copilot-theorem contains unused language pragmas. To comply with our coding style, which required unused code not to be included in the codebase, those pragmas should be removed. This commit removes an unused pragma from Copilot.Theorem.What4. --- 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 c9da7fe8b..51ed6e8ff 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 bbb90b6c8fa777dc2cb088900a5ba5456bac8a49 Mon Sep 17 00:00:00 2001 From: carte731 Date: Thu, 29 May 2025 07:10:00 -0700 Subject: [PATCH 6/8] copilot-theorem: Remove 'LambdaCase' unused pragma from 'Prover.hs'. Refs #613. The code of copilot-theorem contains unused language pragmas. To comply with our coding style, which required unused code not to be included in the codebase, those pragmas should be removed. This commit removes an unused pragma from Copilot.Theorem.Kind2.Prover. --- 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 2d101a7398ae1cc86d4d00f66b4ad0b96f702b84 Mon Sep 17 00:00:00 2001 From: carte731 Date: Thu, 29 May 2025 07:11:08 -0700 Subject: [PATCH 7/8] copilot-theorem: Remove 'LambdaCase' unused pragma from 'SMTIO.hs'. Refs #613. The code of copilot-theorem contains unused language pragmas. To comply with our coding style, which required unused code not to be included in the codebase, those pragmas should be removed. This commit removes an unused pragma from Copilot.Theorem.Prover.SMTIO. --- 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 c9954d663f2988b2db9bd8ce65f9f14e71512195 Mon Sep 17 00:00:00 2001 From: carte731 Date: Thu, 29 May 2025 09:24:36 -0700 Subject: [PATCH 8/8] copilot-theorem: Document changes in CHANGELOG. Refs #613. --- copilot-theorem/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index f221aec44..d28cc3041 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,3 +1,6 @@ +2025-05-29 + * Removed unused pragmas. (#613) + 2025-05-07 * Version bump (4.4). (#618) * Translate quantifiers correctly in Kind2 backend. (#594)