Skip to content
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

Per-module compilation #2468

Merged
merged 85 commits into from
Dec 30, 2023
Merged

Per-module compilation #2468

merged 85 commits into from
Dec 30, 2023

Conversation

lukaszcz
Copy link
Collaborator

@lukaszcz lukaszcz commented Oct 24, 2023

Changes checklist

  • Abstract out data types for stored module representation (ModuleInfo in Juvix.Compiler.Store.Language)
  • Adapt the parser to operate per-module
  • Adapt the scoper to operate per-module
  • Adapt the arity checker to operate per-module
  • Adapt the type checker to operate per-module
  • Adapt Core transformations to operate per-module
  • Adapt the pipeline functions in Juvix.Compiler.Pipeline
  • Add Juvix.Compiler.Pipeline.Driver which drives the per-module compilation process
  • Implement module saving / loading in Pipeline.Driver
  • Detect cyclic module dependencies in Pipeline.Driver
  • Cache visited modules in memory in Pipeline.Driver to avoid excessive disk operations and repeated hash re-computations
  • Recompile a module if one of its dependencies needs recompilation and contains functions that are always inlined.
  • Fix identifier dependencies for mutual block creation in Internal.fromConcrete
    - Fixed by making textually later definitions depend on earlier ones.
    - Now instances are used for resolution only after the textual point of their definition.
    - Similarly, type synonyms will be unfolded only after the textual point of their definition.
  • Fix CLI
  • Fix REPL
  • Fix highlighting
  • Fix HTML generation
  • Adapt test suite

@lukaszcz lukaszcz added enhancement New feature or request core Related to JuvixCore modules labels Oct 24, 2023
@lukaszcz lukaszcz added this to the 0.5.4 milestone Oct 24, 2023
@lukaszcz lukaszcz self-assigned this Oct 24, 2023
@lukaszcz lukaszcz force-pushed the per-module-compilation branch 3 times, most recently from f60a0c4 to bee4360 Compare November 7, 2023 19:37
@jonaprieto jonaprieto modified the milestones: 0.5.4, 0.5.5 Nov 17, 2023
@lukaszcz lukaszcz marked this pull request as ready for review December 22, 2023 16:17
@janmasrovira janmasrovira merged commit 75bce8f into main Dec 30, 2023
8 checks passed
@janmasrovira janmasrovira deleted the per-module-compilation branch December 30, 2023 19:15
lukaszcz added a commit that referenced this pull request May 14, 2024
…ter their inductive types (#2768)

* Closes #2763. 
* Fixes a bug in the scoper, likely introduced in
#2468 by making later declarations
depend on earlier ones. The problem was that the inductive modules were
always added at the beginning of a section, which resulted in an
incorrect definition dependency graph (an inductive type depended on its
associated projections).
* Now inductive modules are added just after a group of inductive
definitions, before the next function definition. This implies that
inductive type definitions which depend on each other cannot be
separated by function definitions. Existing Juvix code needs to be
adjusted.
* The behaviour is now equivalent to "manually" inserting module
declarations with projections after each group of inductive definitions.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
core Related to JuvixCore enhancement New feature or request modules refactor
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Per-module compilation
3 participants