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

Remove compilation #20

Merged
amyliao merged 7 commits from VojtechStep/mikan:feature/compilern't into main 2026年04月25日 03:03:05 +02:00
Contributor
Copy link

Works towards #1.

  • Remove the GHC and JS backends
  • Remove treeless syntax and infra for codegen compilers
  • Remove compilation tests
Works towards #1. - [X] Remove the GHC and JS backends - [X] Remove treeless syntax and infra for codegen compilers - [X] Remove compilation tests

We might actually want to keep COMPILE, it could be a handy way to associate metadata to names for e.g. HTML generation. But the COMPILE GHC stuff, that can go.

(The 1lab's code folding nonsense has a hardcoded list of exceptions which could be replaced by a {-# COMPILE 1Lab ⟨_,_⟩ nofold #-} or something like that).

We might actually want to keep `COMPILE`, it could be a handy way to associate metadata to names for e.g. HTML generation. But the `COMPILE GHC` stuff, that can go. (The 1lab's code folding nonsense has a hardcoded list of exceptions which could be replaced by a `{-# COMPILE 1Lab ⟨_,_⟩ nofold #-}` or something like that).
Author
Contributor
Copy link

Sure thing

Sure thing
VojtechStep force-pushed feature/compilern't from 3a34f93084
Some checks failed
ci/woodpecker/pr/test Pipeline failed
to 4550bec8b4
Some checks are pending
ci/woodpecker/pr/test Pipeline is pending approval
2026年04月23日 23:16:05 +02:00 Compare
VojtechStep force-pushed feature/compilern't from 4550bec8b4
Some checks are pending
ci/woodpecker/pr/test Pipeline is pending approval
to 70d3666753
Some checks failed
ci/woodpecker/pr/test Pipeline failed
2026年04月23日 23:29:18 +02:00 Compare
Author
Contributor
Copy link

I removed the --compile-dir option since nothing was using it, let me know if I should revert that. On the other hand I didn't remove the --no-main option, but I might as well? I don't see a use case for manually overriding it for a non-codegen backend

I removed the `--compile-dir` option since nothing was using it, let me know if I should revert that. On the other hand I didn't remove the `--no-main` option, but I might as well? I don't see a use case for manually overriding it for a non-codegen backend
VojtechStep changed title from (削除) WIP: Remove compilation (削除ここまで) to Remove compilation 2026年04月23日 23:49:20 +02:00
VojtechStep force-pushed feature/compilern't from 70d3666753
Some checks failed
ci/woodpecker/pr/test Pipeline failed
to 6f83fa4713
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
2026年04月24日 22:46:58 +02:00 Compare
amyliao force-pushed feature/compilern't from 6f83fa4713
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
to 45b19304de
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
2026年04月25日 01:15:35 +02:00 Compare
VojtechStep force-pushed feature/compilern't from 45b19304de
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
to 9a70eb0811
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
2026年04月25日 02:10:40 +02:00 Compare
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
2 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!20
Reference in a new issue
1lab/mikan
No description provided.
Delete branch "VojtechStep/mikan:feature/compilern't"

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?