port to Elpi 2.0 #719
Merged
port to Elpi 2.0 #719
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Closed
|
coq CI pr merged |
pi8027
reviewed
Dec 5, 2024
| @@ -50,6 +56,10 @@ let rec inlogpath q = function | |||
| | [] -> [] | |||
| | x :: xs -> (Libnames.string_of_qualid q ^ "/" ^ x) :: inlogpath q xs | |||
|
|
|||
| let warning_legacy_typecheck = | |||
| CWarnings.create ~default:CWarnings.AsError ~name:"elpi.typecheck-syntax" ~category:Coq_elpi_utils.elpi_depr_cat (fun () -> | |||
| Pp.strbrk "The command 'Elpi Typecheck' is deprecated (and does nothing) since type checking is now performed by 'Elpi Accumulate'.") | |||
There was a problem hiding this comment.
Why is this an error by default?
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The main visible change in Elpi 2.0 is that the compiler performs type checking incrementally (as units gets added to the base program) and reports error messages with a precise location. The new type checker is written in OCaml and is much faster, but a bit less permissive. Before this PR all type declarations were merged together before type checking the entire program. With Elpi 2.0 compilation units need to type check using the types declared inside them (or in the base they extend).
Elpi Typecheckbecomes useless.A subtle difference is that rules belonging to a Db are type checked against the Db only, not the programs that uses them or the program that generates them.
This means Db rules "work" in the context of any Db user. But rules cannot call any of the code of these programs (the type checker complains about undefined symbols). Unless the types of the predicates they call are also declared in the Db (not necessarily their code: ensuring that the code is finally available is left to the programmer for now).
Elpi Accumulate dbname File name.can mitigate this issue by putting innamethe code (or at least the type declarations) needed by the rules in the Db.This PR also adds
Elpi File name code.to declare a (virtual) file that can be easily accumulated to Dbs or Programs.This PR also adds a scope attribute to
Elpi Accumulate, in particular#[superglobal] Elpi Accumulate dbname File stuffensure the Db always contains stuff (a bit like it did always contain its header).This PR adds a new command
Elpi Accumulate Db Headerto accumulate the header (type declaration typically) of a Db but not its code. The idiom is to accumulate the Db header early and the Db contents late. This can speed up the (re)compilation of large programs when the db is extended.This PR adds a new command
Elpi Accumulate File Signatureto accumulate the types of a File but not its code.