search

idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.46k stars 369 forks source link

Incremental compilation includes some but not all metas #3337

Open cypheon opened 3 days ago

cypheon commented 3 days ago

In incremental compilation mode, some, but not all metas are compiled. This inconsistency leads to problems for codegen backends which require a definition for all used symbols. I noticed this while working on the LLVM backend, but the root cause seems to be present for all backends (in dynamic languages like Scheme it just doesn't do any real damage).

Steps to Reproduce

Idris 2, version 0.7.0-57f455d13

Compiling the file CompiledMeta.idr (a minimized version of base/Control/Function.idr) via:

idris2 --inc chez --check CompiledMeta.idr

And look at the resulting Chez Scheme ".ss" file.

Expected Behavior

I'm not really sure, what the correct behaviour should be. But I think it should be guaranteed, that the resulting file is internally consistent and all referenced identifiers from the current module are defined. So either all metas should be included in the incremental compile data, or none.

Another way to solve this would be to compile all references to metas as (runtime) errors, like this. But that seems like just treating the symptoms instead of the root cause. Also I'm not sure if that could lead to other problems.

Observed Behavior

In the resulting file CompiledMeta.ss, the identifier CompiledMeta-f2-1244 is referenced 2 times, but never defined. This is fine for Scheme as long as CompiledMeta-x1-1255 is never called, but leads to problems in other backends, where all referenced symbols must be resolvable.

(define CompiledMeta-biinjective (lambda (arg-4 arg-5 arg-6 arg-7 arg-8 ext-0) (((((arg-4 arg-5) arg-6) arg-7) arg-8) ext-0)))
(define CompiledMeta-injective (lambda (arg-3 arg-4 arg-5 ext-0) (((arg-3 arg-4) arg-5) ext-0)))
(define CompiledMeta-x2-1246 (lambda (ext-0 ext-1 ext-2 ext-3 ext-4 ext-5 ext-6 ext-7 ext-8 ext-9 ext-10 ext-11) ext-11))
(define CompiledMeta-y2-1247 (lambda (ext-0 ext-1 ext-2 ext-3 ext-4 ext-5 ext-6 ext-7 ext-8 ext-9 ext-10 ext-11) ext-10))
(define CompiledMeta-v1-1248 (lambda (ext-0 ext-1 ext-2 ext-3 ext-4 ext-5 ext-6 ext-7 ext-8 ext-9 ext-10 ext-11) ext-9))
(define CompiledMeta-w1-1249 (lambda (ext-0 ext-1 ext-2 ext-3 ext-4 ext-5 ext-6 ext-7 ext-8 ext-9 ext-10 ext-11) ext-8))
(define CompiledMeta-x1-1255 (lambda (ext-0 ext-1 ext-2 ext-3 ext-4 ext-5 ext-6 ext-7 ext-8 ext-9 ext-10 ext-11)
  (((((((((((((((CompiledMeta-f2-1244) ext-0) ext-1) ext-2) ext-3) ext-4) ext-5) ext-6) ext-7) ext-8) ext-9) ext-10) ext-11) ext-11) ext-9)))
(define CompiledMeta-y1-1256 (lambda (ext-0 ext-1 ext-2 ext-3 ext-4 ext-5 ext-6 ext-7 ext-8 ext-9 ext-10 ext-11)
  (((((((((((((((CompiledMeta-f2-1244) ext-0) ext-1) ext-2) ext-3) ext-4) ext-5) ext-6) ext-7) ext-8) ext-9) ext-10) ext-11) ext-10) ext-8)))
(define CompiledMeta-u--biinjective_Biinjective_C-40C-40C-46C-58C-32C-36g1C-41C-32C-36f3C-41 (lambda (arg-4 arg-5 arg-6 arg-7 arg-8 arg-9 arg-10 arg-11 ext-0) (((((arg-6 arg-8) arg-9) arg-10) arg-11) (((arg-7 ((arg-4 arg-8) arg-10)) ((arg-4 arg-9) arg-11)) ext-0))))
(define CompiledMeta-u--__Impl_Biinjective_C-40C-40C-46C-58C-32C-36g1C-41C-32C-36f3C-41 (lambda (arg-4 arg-5 arg-6 arg-7 ext-0 ext-1 ext-2 ext-3 ext-4) (CompiledMeta-u--biinjective_Biinjective_C-40C-40C-46C-58C-32C-36g1C-41C-32C-36f3C-41 arg-4 arg-5 arg-6 arg-7 ext-0 ext-1 ext-2 ext-3 ext-4)))