`copilot-theorem`: Code contains unused pragmas

[ivanperez-keera]

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 hPrint"}
- ignore: {name: "Use or"}
- ignore: {name: "Use fmap"}
- ignore: {name: "Use if"}
- ignore: {name: "Use <$>"}
- 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 hPrint"}
- ignore: {name: "Use or"}
- ignore: {name: "Use fmap"}
- ignore: {name: "Use if"}
- ignore: {name: "Use <$>"}
- ignore: {name: "Eta reduce"}

Proposed solution

Remove all unused PRAGMAS from the code in copilot-theorem.

Further notes

None.

[ivanperez-keera]

Change Manager: Confirmed that the issue exists.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.

[ivanperez-keera]

Technical Lead: Issue scheduled for fixing in Copilot 4.5.

Fix assigned to: @carte731.

[carte731]

cpt_613.txt Update: generated text file with 'hlint' and currently I'm working through the document looking for unused pragmas.

[carte731]

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 file

copilot-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.

[carte731]

Items removed. I will conduct compiling testing and pull-request tomorrow (05-30-2025).

[carte731]

Implementor: Solution implemented, review requested.

[carte731]

Implementor: Fix implemented, review requested.

[ivanperez-keera]

Change Manager: Verified that:

• Solution is implemented:
  • [X] The code proposed compiles and passes all tests. Details: Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/275653840
  • [X] The solution proposed produces the expected result. Details: The following dockerfile runs hlint on copilot-theorem with 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:

    --- Dockerfile-verify-613
    FROM ubuntu:jammy
    
    ENV DEBIAN_FRONTEND=noninteractive
    
    RUN apt-get update
    
    RUN apt-get install --yes git
    RUN apt-get install --yes hlint
    
    ADD ignore.yaml /tmp/ignore.yaml
    
    RUN hlint --version
    
    SHELL ["/bin/bash", "-c"]
    CMD git clone $REPO \
        && cd $NAME \
        && git checkout $COMMIT \
        && hlint -h /tmp/ignore.yaml copilot-theorem/src \
        && echo "Success"
    
    --- ignore.yaml
    - 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"}
    

    Command (substitute variables based on new path after merge):

    $ docker run -e REPO=https://github.com/carte731/copilot -e NAME=copilot -e COMMIT=c9954d663f2988b2db9bd8ce65f9f14e71512195 copilot-verify-613
    

• [X] Implementation is documented. Details: No updates needed; the PR removes pragmas but does not otherwise alter or add code.
• [X] Change history is clear.
• [X] Commit messages are clear.
• [X] Changelogs are updated.
• [X] Examples are updated. Details: No updates needed; the PR removes pragmas but does not otherwise alter or add code, nor are examples affected.
• [X] Author is internal or has provided signed CLA.
• [X] Required version bumps are evaluated. Details: Bump not needed; change removes pragmas but does not affect the public API.

[ivanperez-keera]

Change Manager: Implementation ready to be merged.