Skip to content

copilot-theorem: Remove unused pragmas. Refs #613. #638

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Conversation

carte731
Copy link
Collaborator

@carte731 carte731 commented Jul 2, 2025

Remove unused pragmas from copilot-theorem and update the changed logs, as prescribed in the solution proposed for #613.

This PR is a continuation of #630.

carte731 added 8 commits July 2, 2025 16:41
…om 'what4.hs'. Refs Copilot-Language#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.
…efs Copilot-Language#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.
…4.hs'. Refs Copilot-Language#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.
…s'. Refs Copilot-Language#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.
…. Refs Copilot-Language#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.
…Refs Copilot-Language#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.
…efs Copilot-Language#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.
@carte731 carte731 changed the title copilot-theorem: Remove unused pragmas. Refs #613 copilot-theorem: Remove unused pragmas. Refs #613. Jul 2, 2025
@ivanperez-keera
Copy link
Member

Change Manager: Verified that:

  • Solution is implemented:
    • The code proposed compiles and passes all tests. Details:
      Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/275653840
    • 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
      
  • Implementation is documented. Details:
    No updates needed; the PR removes pragmas but does not otherwise alter or add code.
  • Change history is clear.
  • Commit messages are clear.
  • Changelogs are updated.
  • Examples are updated. Details:
    No updates needed; the PR removes pragmas but does not otherwise alter or add code, nor are examples affected.
  • Author is internal or has provided signed CLA.
  • Required version bumps are evaluated. Details:
    Bump not needed; change removes pragmas but does not affect the public API.

@ivanperez-keera ivanperez-keera merged commit e95cc62 into Copilot-Language:master Jul 5, 2025
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Development

Successfully merging this pull request may close these issues.

2 participants