Repository navigation
copilot-theorem: Code contains unused pragmas #613
Description
Description
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.
Type
- Management: comply with styling requirement.
Additional context
None.
Requester
- Ivan Perez.
Method to check presence of bug
Not applicable (not a bug).
Expected result
The code contains no unused pragmas. Running hlint with the following auxiliary file indicates that there are no unused PRAGMAS.
- ignore: {name: "Redundant bracket"}
- ignore: {name: "Use infix"}
- ignore: {name: "Redundant as"}
- ignore: {name: "Redundant <$>"}
- ignore: {name: "Use camelCase"}
- ignore: {name: "Avoid lambda"}
- ignore: {name: "Use gets"}
- ignore: {name: "Redundant $"}
- ignore: {name: "Use <&>"}
- ignore: {name: "Use concatMap"}
- ignore: {name: "Move brackets to avoid $"}
- ignore: {name: "Use /="}
- ignore: {name: "Use newtype instead of data"}
- ignore: {name: "Use :"}
- ignore: {name: "Replace case with fromMaybe"}
- ignore: {name: "Use >=>"}
- ignore: {name: "Use curry"}
- ignore: {name: "Use first"}
- ignore: {name: "Use hPrint"}
- ignore: {name: "Use or"}
- ignore: {name: "Use fmap"}
- ignore: {name: "Use if"}
- ignore: {name: "Use <$>"}
- ignore: {name: "Reduce duplication"}
- ignore: {name: "Eta reduce"}
Desired result
The code contains no unused pragmas. Running hlint with the following auxiliary file indicates that there are no unused PRAGMAS.
- ignore: {name: "Redundant bracket"}
- ignore: {name: "Use infix"}
- ignore: {name: "Redundant as"}
- ignore: {name: "Redundant <$>"}
- ignore: {name: "Use camelCase"}
- ignore: {name: "Avoid lambda"}
- ignore: {name: "Use gets"}
- ignore: {name: "Redundant $"}
- ignore: {name: "Use <&>"}
- ignore: {name: "Use concatMap"}
- ignore: {name: "Move brackets to avoid $"}
- ignore: {name: "Use /="}
- ignore: {name: "Use newtype instead of data"}
- ignore: {name: "Use :"}
- ignore: {name: "Replace case with fromMaybe"}
- ignore: {name: "Use >=>"}
- ignore: {name: "Use curry"}
- ignore: {name: "Use first"}
- ignore: {name: "Use hPrint"}
- ignore: {name: "Use or"}
- ignore: {name: "Use fmap"}
- ignore: {name: "Use if"}
- ignore: {name: "Use <$>"}
- ignore: {name: "Reduce duplication"}
- ignore: {name: "Eta reduce"}Proposed solution
Remove all unused PRAGMAS from the code in copilot-theorem.
Further notes
None.
Activity
[-]`copilot-theorem`: Code contains unused PRAGMAS[/-][+]`copilot-theorem`: Code contains unused pragmas[/+]ivanperez-keera commentedon Mar 29, 2025
Change Manager: Confirmed that the issue exists.
ivanperez-keera commentedon Mar 29, 2025
Technical Lead: Confirmed that the issue should be addressed.
ivanperez-keera commentedon May 13, 2025
Technical Lead: Issue scheduled for fixing in Copilot 4.5.
Fix assigned to: @carte731.
carte731 commentedon May 29, 2025
cpt_613.txt
Update: generated text file with 'hlint' and currently I'm working through the document looking for unused pragmas.
carte731 commentedon May 29, 2025
Current listing of unused pragmas in Copilot-Theorem:
copilot-theorem/src/Copilot/Theorem/What4.hs:4:1-43: Warning: Unused LANGUAGE pragma
Found:
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
Perhaps you should remove it.
copilot-theorem/src/Copilot/Theorem/What4.hs:7:1-43: Warning: Unused LANGUAGE pragma
Found:
{-# LANGUAGE MultiWayIf #-}
Perhaps you should remove it.
copilot-theorem/src/Copilot/Theorem/What4.hs:11:1-43: Warning: Unused LANGUAGE pragma
Found:
{-# LANGUAGE StandaloneDeriving #-}
Perhaps you should remove it.
copilot-theorem/src/Copilot/Theorem/What4.hs:12:1-43: Warning: Unused LANGUAGE pragma
Found:
{-# LANGUAGE TemplateHaskell #-}
Perhaps you should remove it.
Note: may require
{-# LANGUAGE TemplateHaskellQuotes #-}adding to the top of the filecopilot-theorem/src/Copilot/Theorem/What4.hs:13:1-43: Warning: Unused LANGUAGE pragma
Found:
{-# LANGUAGE TupleSections #-}
Perhaps you should remove it.
copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs:1:1-28: Warning: Unused LANGUAGE pragma
Found:
{-# LANGUAGE LambdaCase #-}
Perhaps you should remove it.
copilot-theorem/src/Copilot/Theorem/Prover/SMTIO.hs:1:1-31: Warning: Unused LANGUAGE pragma
Found:
{-# LANGUAGE LambdaCase #-}
Perhaps you should remove it.
7 remaining items
copilot-theorem: Remove 'GeneralizedNewtypeDeriving' unused pragma fr…
copilot-theorem: Remove 'MultiWayIf' unused pragma from 'what4.hs'. R…
copilot-theorem: Remove 'StandaloneDeriving' unused pragma from 'what…
copilot-theorem: Remove 'TemplateHaskell' unused pragma from 'what4.h…
copilot-theorem: Remove 'TupleSections' unused pragma from 'what4.hs'…
copilot-theorem: Remove 'LambdaCase' unused pragma from 'Prover.hs'. …
copilot-theorem: Remove 'LambdaCase' unused pragma from 'SMTIO.hs'. R…
copilot-theorem: Document changes in CHANGELOG. Refs Copilot-Language…
carte731 commentedon Jul 3, 2025
Implementor: Fix implemented, review requested.
ivanperez-keera commentedon Jul 5, 2025
Change Manager: Verified that:
Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/275653840
The following dockerfile runs hlint on
copilot-theoremwith the provided list of ignored warnings, which does not include unnecessary language pragmas, and checks that there are no warnings reported, after which it prints the message success:No updates needed; the PR removes pragmas but does not otherwise alter or add code.
No updates needed; the PR removes pragmas but does not otherwise alter or add code, nor are examples affected.
Bump not needed; change removes pragmas but does not affect the public API.
ivanperez-keera commentedon Jul 5, 2025
Change Manager: Implementation ready to be merged.
Merge branch 'develop-remove-pragmas-theorem'. Close Copilot-Language…