1lab/mikan
13
52
Fork
You've already forked mikan
9

chore/fix: unbreak larger parts of make test #136

Open
fogti wants to merge 1 commit from fogti/mikan:chore-make-test into main
pull from: fogti/mikan:chore-make-test
merge into: 1lab:main
1lab:main
1lab:aliao/occurs-opt
1lab:aliao/rec-con
1lab:fix-license
1lab:aliao/oopsie
1lab:aliao/strengthen-iapply
Contributor
Copy link

Currently, make test is just completely broken.

This PR makes Mikan_datadir=src/data/ MIKAN_BIN=$(realpath ./dist-*/build/mikan/mikan) make test mostly work (except for the cubical test suite...:)

 Checking Agda.Builtin.Float (mikan/cubical/src/data/lib/prim/Agda/Builtin/Float.agda).
 Checking Agda.Builtin.Int (mikan/cubical/src/data/lib/prim/Agda/Builtin/Int.agda).
 Checking Cubical.Reflection.Base (mikan/cubical/Cubical/Reflection/Base.agda).
mikan/cubical/cubical.agda-lib:1.1: warning: -W[no]OptionRedundant
Option --cubical no longer has any effect, and is only accepted for compatibility.
when scope checking the declaration
 open import Cubical.Reflection.Base
mikan/cubical/cubical.agda-lib:1.1: warning: -W[no]OptionRedundant
Option --guardedness no longer has any effect, and is only accepted for compatibility.
when scope checking the declaration
 open import Cubical.Reflection.Base
mikan/cubical/Cubical/Reflection/Base.agda:30.1-85: error: [NoParseForLHS]
Could not parse the pattern synonym right-hand side
R.arg (R.arg-info R.visible (R.modality R.relevant R.quantity-ω)) t
Problematic expression: ((R.modality R.relevant) R.quantity-ω)
Operators used in the grammar:
 None
when scope checking the declaration
 pattern varg t = R.arg
 (R.arg-info R.visible (R.modality R.relevant R.quantity-ω)) t
make[2]: *** [GNUmakefile:32: check] Error 42
make[2]: Leaving directory 'mikan/cubical'
make[1]: *** [GNUmakefile:13: build] Error 2
make[1]: Leaving directory 'mikan/cubical'
Currently, `make test` is just completely broken. This PR makes `Mikan_datadir=src/data/ MIKAN_BIN=$(realpath ./dist-*/build/mikan/mikan) make test` mostly work (except for the `cubical` test suite...:) ``` Checking Agda.Builtin.Float (mikan/cubical/src/data/lib/prim/Agda/Builtin/Float.agda). Checking Agda.Builtin.Int (mikan/cubical/src/data/lib/prim/Agda/Builtin/Int.agda). Checking Cubical.Reflection.Base (mikan/cubical/Cubical/Reflection/Base.agda). mikan/cubical/cubical.agda-lib:1.1: warning: -W[no]OptionRedundant Option --cubical no longer has any effect, and is only accepted for compatibility. when scope checking the declaration open import Cubical.Reflection.Base mikan/cubical/cubical.agda-lib:1.1: warning: -W[no]OptionRedundant Option --guardedness no longer has any effect, and is only accepted for compatibility. when scope checking the declaration open import Cubical.Reflection.Base mikan/cubical/Cubical/Reflection/Base.agda:30.1-85: error: [NoParseForLHS] Could not parse the pattern synonym right-hand side R.arg (R.arg-info R.visible (R.modality R.relevant R.quantity-ω)) t Problematic expression: ((R.modality R.relevant) R.quantity-ω) Operators used in the grammar: None when scope checking the declaration pattern varg t = R.arg (R.arg-info R.visible (R.modality R.relevant R.quantity-ω)) t make[2]: *** [GNUmakefile:32: check] Error 42 make[2]: Leaving directory 'mikan/cubical' make[1]: *** [GNUmakefile:13: build] Error 2 make[1]: Leaving directory 'mikan/cubical' ```
fogti force-pushed chore-make-test from 4fe972d0f9
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
to 6adbf946c5
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
2026年06月18日 20:44:39 +02:00 Compare

Thank you for your contribution! I'd like to get word from @totbwf before we go ahead with merging this.

In my understanding our plan was to get rid of the Makefile-based workflow entirely, telling contributors to use the Cabal commands instead; however, the build system simplification plan wasn't my plan, so it's possible that we're actually keeping the Makefile and this should be merged.

Thank you for your contribution! I'd like to get word from @totbwf before we go ahead with merging this. In my understanding our plan was to get rid of the `Makefile`-based workflow entirely, telling contributors to use the Cabal commands instead; however, the build system simplification plan wasn't *my* plan, so it's possible that we're actually keeping the Makefile and this should be merged.

I can confirm that plan is to work towards a makefile-free future. Currently, all the tests do run and pass under cabal test, so these makefile targets are no longer needed. I'd be inclined to just delete them outright, along with any other targets that use cabal v1. Keeping them suggests that we support the legacy makefile workflow, which is a maintainence burden I don't think anyone wants to shoulder.

We do need to keep the makefile around for some other purposes (building docs, etc) while we work out a more permanent solution there, so we can't just delete the whole thing yet.

I can confirm that plan is to work towards a makefile-free future. Currently, all the tests do run and pass under `cabal test`, so these makefile targets are no longer needed. I'd be inclined to just delete them outright, along with any other targets that use cabal v1. Keeping them suggests that we support the legacy makefile workflow, which is a maintainence burden I don't think anyone wants to shoulder. We do need to keep the makefile around for some other purposes (building docs, etc) while we work out a more permanent solution there, so we can't just delete the whole thing yet.
Author
Contributor
Copy link

Should I split the formatting and cabal.project.* fixes into a separate PR (given that they're useful independent of the Makefile workflow)?

Should I split the formatting and `cabal.project.*` fixes into a separate PR (given that they're useful independent of the `Makefile` workflow)?

I think we can keep this PR open but change it to removing whatever targets have been superceded from the Makefile?

I think we can keep this PR open but change it to removing whatever targets have been superceded from the Makefile?

Yeah, that seems like a good idea to me!

Yeah, that seems like a good idea to me!
Author
Contributor
Copy link

Does that mean just removing the entire test target and its subtargets?

Does that mean just removing the entire `test` target and its subtargets?
fogti force-pushed chore-make-test from 6adbf946c5
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
to 897f506226
Some checks are pending
ci/woodpecker/pr/test Pipeline is pending approval
2026年06月27日 09:16:53 +02:00 Compare
Some checks are pending
ci/woodpecker/pr/test Pipeline is pending approval
This pull request can be merged automatically.
This branch is out-of-date with the base branch
You are not authorized to merge this pull request.
View command line instructions

Checkout

From your project repository, check out a new branch and test the changes.
git fetch -u chore-make-test:fogti-chore-make-test
git switch fogti-chore-make-test

Merge

Merge the changes and update on Forgejo.

Warning: The "Autodetect manual merge" setting is not enabled for this repository, you will have to mark this pull request as manually merged afterwards.

git switch main
git merge --no-ff fogti-chore-make-test
git switch fogti-chore-make-test
git rebase main
git switch main
git merge --ff-only fogti-chore-make-test
git switch fogti-chore-make-test
git rebase main
git switch main
git merge --no-ff fogti-chore-make-test
git switch main
git merge --squash fogti-chore-make-test
git switch main
git merge --ff-only fogti-chore-make-test
git switch main
git merge fogti-chore-make-test
git push origin main
Sign in to join this conversation.
No reviewers
Labels
Clear labels
1 - scope
language
 Backwards-compatible changes to the surface language, such as adding new features.
1 - scope
language change
 Breaking changes to a documented part of the surface language. These should be documented and specifically called out in the changelog.
1 - scope
performance
 Semantics-preserving performance work.
1 - scope
task
 Changes that are not apparent to the user, e.g. developer documentation and refactors, which do not need to be documented.
A: dead-code
Dead code elimination and --save-metas.
A: errors
Reporting of error and warning messages.
A: highlighting
Highlighting during interaction & literate compilation
A: imports
Handling of imports and interface file de/serialization.
A: infra
Iinfrastructure (e.g. CI, developer documentation, the build system, or the repository itself)
A: instance
Instance declarations, arguments, and resolution
A: lhs
LHS checking, coverage checking, and clause compilation
A: modules
Declaration and instantiation of parametrised modules.
A: parallel
Parallel typechecking.
A: positivity
Positivity checking
A: printing
Pretty-printing, display forms, and the wording of diagnostic messages
A: records
Record declarations, record expressions and copattern matching
A: scoping
Scope checking (ConcreteToAbstract)
A: termination
Termination checking
0 - type
bug
 Issues describing an incorrect behaviour in the project, typos in the documentation, etc.
0 - type
discussion
 An issue raised to gather opinions on a proposed change, or a suggested language change.
0 - type
question
 An issue raised to ask a question.
9 - status
duplicate
 This issue or pull request already exists.
9 - status
info needed
 More information is needed from the submitter to decide how to proceed with the issue report.
9 - status
invalid
 The issue report or pull request does not describe an actual bug, or does otherwise does not meet the contributing guidelines.
good first issue
Interested in contributing? Get started here.
upstream
Related to an upstream repository, already reported there
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
3 participants
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference
1lab/mikan!136
Reference in a new issue
1lab/mikan
No description provided.
Delete branch "fogti/mikan:chore-make-test"

Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?