From 291fdd19376097850acdf5b8068472b801a2357c Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Wed, 2 Feb 2022 23:15:50 -0500 Subject: [PATCH 01/30] Separate compilation doc. --- text/separate-compilation.md | 197 +++++++++++++++++++++++++++++++++++ 1 file changed, 197 insertions(+) create mode 100644 text/separate-compilation.md diff --git a/text/separate-compilation.md b/text/separate-compilation.md new file mode 100644 index 00000000..592bb5ee --- /dev/null +++ b/text/separate-compilation.md @@ -0,0 +1,197 @@ +- Title: Separate Compilation in Coq + +- Drivers: David Swasey, Paolo Giarrusso, Gregory Malecha + +# Summary + +Coq provides a module system that can be used explicitly through commands such as `Module` and `Module Type`. These can be quite heavyweight in many instances, and have some limitations when it comes to separately compiling files and building generic libraries. The ideas are drawn from OCaml, where .mli files can be used to express the interface of a module separately from its implementation. In addition to build parallelism, this also enables: +Avoiding dependencies that are only needed for non-exposed definitions, e.g. you do not need to expose the fact that proofs are constructed using particular tactics. +Build parallelism (even without using -vos builds) because clients can be compiled against specification files only. + +This CEP proposes several bits of sugar that makes it easier to use modules and achieve separate compilation. + +# Proposal + +At the highest level, this proposal introduces the concept of an interface file with a .vi extension. An example of a .vi and .v file for a simple module would be the following: + +``` +(* lib.vi *) +Parameter value : nat. +Axiom value_is_42 : value = 42. + +(* lib.v *) +Definition value : nat := 42. +Definition value_is_42 : value = 42 := ltac:(reflexivity). +``` + +Conceptually, this pair of files could be compiled to the following single Coq file: + +``` +(* lib_composed.v: *) +Module Type LIB. + Parameter value : nat. + Axiom value_is_42 : value = 42. +End LIB. + +Module lib : LIB. + Definition value : nat := 42. + Definition value_is_42 : value = 42 := ltac:(reflexivity). +End lib. + +Export lib. (* make the declarations from lib available from [Import]ing lib (rather that lib.lib *) +``` + +## Semantics + +In this section we sketch the semantics informally — ignoring problems due to universe constraints until the relevant subsections. + +.vi interfaces are meant to hide implementations and support separate compilation in Cardelli's sense. Hence, a module `consumer.v` that consumes the interface of `producer.vi` shall be compiled without inspecting either `producer.v`, any build product from `producer.v`, or even the existence of `producer.v`. As a consequence, no change to `producer.v` can affect whether `consumer.v` typechecks. + +Because Coq modules do not satisfy subsumption, removing `.vi` files can expose implementation details that break clients. This is a feature. + +`.vi` interfaces can hide `Require`-bound side effects. Hiding is also an intentional feature, that is supported automatically in the above compilation model. However, this feature is not supported today, either via existing `vos` builds or via opaque ascription. [One can write a Require in an interactive module, but Coq complains enough we have not explored what happens. If we lift the Require out into the surrounding top-level module, its side effects cannot be hidden.] + +### "Link-time" Universe Checking + +Cardelli's separate compilation has a further demand: in this example, if `consumer.v` typechecks, and `producer.v` satisfies its interface, the two shall link successfully. In Coq this is true except for universe constraints, like for existing `.vos` builds. To alleviate this problem, we propose +extending `.vok` outputs to include proof terms, or at least universe constraints +so that we can run a "link-time checker" that loads the whole program and checks whether combined universe constraints are satisfiable. +The above assumes that universes and universe constraints for a term can be generated in isolation. However, universe inference is sometimes too greedy: when compiling `consumer.v` without the universe constraints from `producer.v`, Coq will sometimes produce different terms. +for instance, some Ltac can fail with an universe inconsistency and backtrack (as mentioned in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/vos.2Fvok.20and.20link-time.20universe.20check); we propose that the extra constraints be hidden at this stage +sometimes, Coq also seems to produce stricter universe constraints than strictly needed, as Gaëtan shows in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Why.20does.20my.20fix.20for.20a.20universe.20problem.20work.3F/near/264903292. It'd be nice if the constraints were produced modularly, even if this might produce bigger graphs (hopefully in a tolerable way), or might require manual eta-expansion (we'd need Coq to give a warning/error when it must eta-expand, suggesting the user do that by hand). + +### "Full compilation" semantics + +It might be desirable to use interfaces even when compiling "vo-style" rather than "vos-style". At least, it would be easier to check universes in such a mode. This means that compiling `consumer.v` would load `producer.vo` despite the existence of `producer.vi`. We propose that in this mode, most side effects of `producer.vo` shall be ignored anyway, including its `Require`-bound side effects. However, the extra universe constraints from `producer.vo` compared to `producer.vos` are important. + +# Implementation + +We speculate this can be accomplished by compiling `.vi` files to `.vos` outputs, and compiling `.v` files into `.vok` files. + +== + +The goal of `.vi` files is to support separate compilation in Cardelli's sense: implementation changes that preserve the interface cannot affect clients. More formally, modules can be typechecked separately, and successful typechecking guarantees successful linking (again, up to universe checking; see below). For clarity, we intend "typechecking" to include all of elaboration, including the execution of proof scripts. If a client `bar.v` of a `foo.vi` interface elaborates correctly to a compiled file (`bar.vo` or `bar.vok`), and if `foo.v` satisfies its interface, + +The semantics of a `.vi` file would resemble today's opaque ascription with module types, while reducing boilerplate. Clients would only see the interface declared in the .vi file, but would not see the definitions of the .v file, nor its non-logical side effects such as hints. + +Unlike today, `.vi` interfaces would hide not just `Import`-bound side effects, but also `Require`-bound ones. [This might be kind-of possible today by hiding `Require` inside modules with opaque ascriptions, but `Require` is discouraged inside interactive modules.] + +A reviewer of our CoqPL paper objected to our proposal, because removing an interface file would reintroduce the hidden side effects and break clients. We consider this not a bug but a feature, essential to separate compilation: any change to the + +### Universes + +As some readers will anticipate, universe checks do not admit fully separate compilation; module bodies might add constraints absent from interfaces. This is already an issue with `.vos` builds today, and is a problem inherent to parallel builds, so any solutions to this problem could be shared. + +We consider vos builds a special case of this proposal, where interfaces are inferred as the strictest possible ones for the given implementation; `.vi` files enable hiding more implementation details. In both cases, the interface omits universe constraints that are derived from hidden bodies (for vos builds, just Qed bodies). While some universe checks are performed anyway, omitted constraints might make the universe graph unsatisfiable. + +To remedy this problem, we propose an additional "global" check. By analogy with separate compilation in other languages, we call this "link-time" universe checking. + +Consider files `a.vi`, `a.v` and `b.v`, where `Title: Separate Compilation in Coq +Authors: David Swasey, Paolo Giarrusso, Gregory Malecha + +# Summary + +Coq provides a module system that can be used explicitly through commands such as `Module` and `Module Type`. These can be quite heavyweight in many instances, and have some limitations when it comes to separately compiling files and building generic libraries. The ideas are drawn from OCaml, where .mli files can be used to express the interface of a module separately from its implementation. In addition to build parallelism, this also enables: +Avoiding dependencies that are only needed for non-exposed definitions, e.g. you do not need to expose the fact that proofs are constructed using particular tactics. +Build parallelism (even without using -vos builds) because clients can be compiled against specification files only. + +This CEP proposes several bits of sugar that makes it easier to use modules and achieve separate compilation. + +# Proposal + +At the highest level, this proposal introduces the concept of an interface file with a .vi extension. An example of a .vi and .v file for a simple module would be the following: + +(* lib.vi *) +Parameter value : nat. +Axiom value_is_42 : value = 42. + +(* lib.v *) +Definition value : nat := 42. +Definition value_is_42 : value = 42 := ltac:(reflexivity). + +Conceptually, this pair of files could be compiled to the following single Coq file: + +(* lib_composed.v: *) +Module Type LIB. + Parameter value : nat. + Axiom value_is_42 : value = 42. +End LIB. + +Module lib : LIB. + Definition value : nat := 42. + Definition value_is_42 : value = 42 := ltac:(reflexivity). +End lib. + +Export lib. (* make the declarations from lib available from [Import]ing lib (rather that lib.lib *) + +## Semantics + +In this section we sketch the semantics informally — ignoring problems due to universe constraints until the relevant subsections. + +.vi interfaces are meant to hide implementations and support separate compilation in Cardelli's sense. Hence, a module `consumer.v` that consumes the interface of `producer.vi` shall be compiled without inspecting either `producer.v`, any build product from `producer.v`, or even the existence of `producer.v`. As a consequence, no change to `producer.v` can affect whether `consumer.v` typechecks. + +Because Coq modules do not satisfy subsumption, removing `.vi` files can expose implementation details that break clients. This is a feature. + +`.vi` interfaces can hide `Require`-bound side effects. Hiding is also an intentional feature, that is supported automatically in the above compilation model. However, this feature is not supported today, either via existing `vos` builds or via opaque ascription. [One can write a Require in an interactive module, but Coq complains enough we have not explored what happens. If we lift the Require out into the surrounding top-level module, its side effects cannot be hidden.] + +### "Link-time" Universe Checking + +Cardelli's separate compilation has a further demand: in this example, if `consumer.v` typechecks, and `producer.v` satisfies its interface, the two shall link successfully. In Coq this is true except for universe constraints, like for existing `.vos` builds. To alleviate this problem, we propose +extending `.vok` outputs to include proof terms, or at least universe constraints +so that we can run a "link-time checker" that loads the whole program and checks whether combined universe constraints are satisfiable. +The above assumes that universes and universe constraints for a term can be generated in isolation. However, universe inference is sometimes too greedy: when compiling `consumer.v` without the universe constraints from `producer.v`, Coq will sometimes produce different terms. +for instance, some Ltac can fail with an universe inconsistency and backtrack (as mentioned in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/vos.2Fvok.20and.20link-time.20universe.20check); we propose that the extra constraints be hidden at this stage +sometimes, Coq also seems to produce stricter universe constraints than strictly needed, as Gaëtan shows in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Why.20does.20my.20fix.20for.20a.20universe.20problem.20work.3F/near/264903292. It'd be nice if the constraints were produced modularly, even if this might produce bigger graphs (hopefully in a tolerable way), or might require manual eta-expansion (we'd need Coq to give a warning/error when it must eta-expand, suggesting the user do that by hand). + +### "Full compilation" semantics + +It might be desirable to use interfaces even when compiling "vo-style" rather than "vos-style". At least, it would be easier to check universes in such a mode. This means that compiling `consumer.v` would load `producer.vo` despite the existence of `producer.vi`. We propose that in this mode, most side effects of `producer.vo` shall be ignored anyway, including its `Require`-bound side effects. However, the extra universe constraints from `producer.vo` compared to `producer.vos` are important. + +# Implementation + +We speculate this can be accomplished by compiling `.vi` files to `.vos` outputs, and compiling `.v` files into `.vok` files. + +== + +The goal of `.vi` files is to support separate compilation in Cardelli's sense: implementation changes that preserve the interface cannot affect clients. More formally, modules can be typechecked separately, and successful typechecking guarantees successful linking (again, up to universe checking; see below). For clarity, we intend "typechecking" to include all of elaboration, including the execution of proof scripts. If a client `bar.v` of a `foo.vi` interface elaborates correctly to a compiled file (`bar.vo` or `bar.vok`), and if `foo.v` satisfies its interface, + +The semantics of a `.vi` file would resemble today's opaque ascription with module types, while reducing boilerplate. Clients would only see the interface declared in the .vi file, but would not see the definitions of the .v file, nor its non-logical side effects such as hints. + +Unlike today, `.vi` interfaces would hide not just `Import`-bound side effects, but also `Require`-bound ones. [This might be kind-of possible today by hiding `Require` inside modules with opaque ascriptions, but `Require` is discouraged inside interactive modules.] + +A reviewer of our CoqPL paper objected to our proposal, because removing an interface file would reintroduce the hidden side effects and break clients. We consider this not a bug but a feature, essential to separate compilation: any change to the + +### Universes + +As some readers will anticipate, universe checks do not admit fully separate compilation; module bodies might add constraints absent from interfaces. This is already an issue with `.vos` builds today, and is a problem inherent to parallel builds, so any solutions to this problem could be shared. + +We consider vos builds a special case of this proposal, where interfaces are inferred as the strictest possible ones for the given implementation; `.vi` files enable hiding more implementation details. In both cases, the interface omits universe constraints that are derived from hidden bodies (for vos builds, just Qed bodies). While some universe checks are performed anyway, omitted constraints might make the universe graph unsatisfiable. + +To remedy this problem, we propose an additional "global" check. By analogy with separate compilation in other languages, we call this "link-time" universe checking. + +Consider files `a.vi`, `a.v` and `b.v`, where `b.v` depends on `a.v`. Assume that `a.v` satisfies the interface in `a.vi` but adds universe constraints, and that `b.v` typechecks against `a.vi`. Moreover, assume that the universe constraints of `a.v` and `b.v` are both satisfiable in isolation. + +We have two problems: + +Composing the universe constraints of `a.v` and `b.v` might produce an unsatisfiable constraint set, but this is not detected. This can also +We can elaborate `a.v` and `b.v` separately, but their combination might produce an unsatisfiable + + +A further issue is that universe inference does not seem to be prone to parallelism. Without seeing `producer.v`, + +## Value + + +b.v` depends on `a.v`. Assume that `a.v` satisfies the interface in `a.vi` but adds universe constraints, and that `b.v` typechecks against `a.vi`. Moreover, assume that the universe constraints of `a.v` and `b.v` are both satisfiable in isolation. + +We have two problems: + +Composing the universe constraints of `a.v` and `b.v` might produce an unsatisfiable constraint set, but this is not detected. This can also +We can elaborate `a.v` and `b.v` separately, but their combination might produce an unsatisfiable + + +A further issue is that universe inference does not seem to be prone to parallelism. Without seeing `producer.v`, + +## Value + + From 5d19d22b927e2b52751ab06bdbca7d8487256169 Mon Sep 17 00:00:00 2001 From: Paolo Giarrusso Date: Wed, 9 Feb 2022 17:34:13 +0000 Subject: [PATCH 02/30] Apply 1 suggestion(s) to 1 file(s) --- text/separate-compilation.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 592bb5ee..d8cb6d20 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -4,7 +4,7 @@ # Summary -Coq provides a module system that can be used explicitly through commands such as `Module` and `Module Type`. These can be quite heavyweight in many instances, and have some limitations when it comes to separately compiling files and building generic libraries. The ideas are drawn from OCaml, where .mli files can be used to express the interface of a module separately from its implementation. In addition to build parallelism, this also enables: +Coq provides a module system that can be used explicitly through commands such as `Module` and `Module Type`. These can be quite heavyweight in many instances, and have some limitations when it comes to separately compiling files and building generic libraries. The ideas are drawn from OCaml, where .mli files can be used to express the interface of a module separately from its implementation. This enables: Avoiding dependencies that are only needed for non-exposed definitions, e.g. you do not need to expose the fact that proofs are constructed using particular tactics. Build parallelism (even without using -vos builds) because clients can be compiled against specification files only. From 8b5e4e9cb8549295a0c2ee966285600c823bb8f7 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Wed, 9 Feb 2022 18:38:19 +0000 Subject: [PATCH 03/30] Update text/separate-compilation.md --- text/separate-compilation.md | 96 +++++++++++++++++++++--------------- 1 file changed, 56 insertions(+), 40 deletions(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index d8cb6d20..8a9a0a98 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -10,9 +10,15 @@ Build parallelism (even without using -vos builds) because clients can be compil This CEP proposes several bits of sugar that makes it easier to use modules and achieve separate compilation. +NOTE: In this proposal we use the extension `.vi` to be analog to `.mli` (derived from `.ml`). Similarly, we use `.vio` as what it compiles to. The `.vio` extension is already used for `-quick` build, so we could use `.vix` or anything else here. Or, remove `-quick` builds entirely and re-purpose the name. + +## Background + +The goal of `.vi` files is to support separate compilation in Cardelli's sense: implementation changes that preserve the interface cannot affect clients. More formally, modules can be typechecked separately, and successful typechecking guarantees successful linking (again, up to universe checking; see below). For clarity, we intend "typechecking" to include all of elaboration, including the execution of proof scripts. If a client `bar.v` of a `foo.vi` interface elaborates correctly to a compiled file (`bar.vo` or `bar.vok`), and if `foo.v` satisfies its interface, + # Proposal -At the highest level, this proposal introduces the concept of an interface file with a .vi extension. An example of a .vi and .v file for a simple module would be the following: +At the highest level, this proposal introduces the concept of an interface file with a `.vi` extension. An example of a `.vi` and `.v` file for a simple module would be the following: ``` (* lib.vi *) @@ -41,6 +47,49 @@ End lib. Export lib. (* make the declarations from lib available from [Import]ing lib (rather that lib.lib *) ``` +With the new file, there are two additional scenarios for considerations: + +1. A `.v` file without a `.vi` file. This *must not* change at all. It is analagous to having a `Module` without an opaque ascription. It is also equivalent to copy-pasting the `.v` file in the corresponding `.vi` file. [^vi-less] +2. A `.vi` file without a `.v` file. In this case, + +[^vi-less]: There is some disagreement here concerning whether the bodies of `Qed`d definitions should be included here. + +/// REMOVE +if .vi is missing then + produce it by dropping the body of Qed definitions + +- after you do this, you only need to consider the .v&.vi case +* in the -vos build when you process a [Require] you get the .vio file +* in the vo build when you process the require, you read the .vio file and the .vo file pulling the universes from the later into the former + +if the .vi is missing then + cp x.v x.vi +- after you do this, you only need to consider the .v&.vi case +* you read the information from .vio file, treat .vio as a .vo + +vos, .vi +vos, .v +vos, .v{,i} +vo, .vi +vo, .v +vo, .v{,i} + + +What are the build dependencies to build: client.v that requires lib. + +``` +# full build with universe checking +lib.vio : lib.vo lib.vi +lib.vo : lib.v + +# partial build (build speedup, no universe checking) +lib.vio : lib.vi +lib.vo : lib.vio lib.v + +client.v : lib.vio +``` +/// END REMOVE + ## Semantics In this section we sketch the semantics informally — ignoring problems due to universe constraints until the relevant subsections. @@ -62,7 +111,9 @@ sometimes, Coq also seems to produce stricter universe constraints than strictly ### "Full compilation" semantics -It might be desirable to use interfaces even when compiling "vo-style" rather than "vos-style". At least, it would be easier to check universes in such a mode. This means that compiling `consumer.v` would load `producer.vo` despite the existence of `producer.vi`. We propose that in this mode, most side effects of `producer.vo` shall be ignored anyway, including its `Require`-bound side effects. However, the extra universe constraints from `producer.vo` compared to `producer.vos` are important. +It might be desirable to use interfaces even when compiling "vo-style" rather than "vos-style". At least, it would be easier to check universes in such a mode. +This means that compiling `consumer.v` would load `producer.vo` despite the existence of `producer.vi`. We propose that in this mode, most side effects of `producer.vo` shall be ignored anyway, including its `Require`-bound side effects. +However, the extra universe constraints from `producer.vo` compared to `producer.vos` are important. # Implementation @@ -70,7 +121,7 @@ We speculate this can be accomplished by compiling `.vi` files to `.vos` outputs == -The goal of `.vi` files is to support separate compilation in Cardelli's sense: implementation changes that preserve the interface cannot affect clients. More formally, modules can be typechecked separately, and successful typechecking guarantees successful linking (again, up to universe checking; see below). For clarity, we intend "typechecking" to include all of elaboration, including the execution of proof scripts. If a client `bar.v` of a `foo.vi` interface elaborates correctly to a compiled file (`bar.vo` or `bar.vok`), and if `foo.v` satisfies its interface, + The semantics of a `.vi` file would resemble today's opaque ascription with module types, while reducing boilerplate. Clients would only see the interface declared in the .vi file, but would not see the definitions of the .v file, nor its non-logical side effects such as hints. @@ -87,7 +138,7 @@ We consider vos builds a special case of this proposal, where interfaces are inf To remedy this problem, we propose an additional "global" check. By analogy with separate compilation in other languages, we call this "link-time" universe checking. Consider files `a.vi`, `a.v` and `b.v`, where `Title: Separate Compilation in Coq -Authors: David Swasey, Paolo Giarrusso, Gregory Malecha +Authors: David Swasey, Paolo Giarrusso, Gregory Malecha` # Summary @@ -97,32 +148,6 @@ Build parallelism (even without using -vos builds) because clients can be compil This CEP proposes several bits of sugar that makes it easier to use modules and achieve separate compilation. -# Proposal - -At the highest level, this proposal introduces the concept of an interface file with a .vi extension. An example of a .vi and .v file for a simple module would be the following: - -(* lib.vi *) -Parameter value : nat. -Axiom value_is_42 : value = 42. - -(* lib.v *) -Definition value : nat := 42. -Definition value_is_42 : value = 42 := ltac:(reflexivity). - -Conceptually, this pair of files could be compiled to the following single Coq file: - -(* lib_composed.v: *) -Module Type LIB. - Parameter value : nat. - Axiom value_is_42 : value = 42. -End LIB. - -Module lib : LIB. - Definition value : nat := 42. - Definition value_is_42 : value = 42 := ltac:(reflexivity). -End lib. - -Export lib. (* make the declarations from lib available from [Import]ing lib (rather that lib.lib *) ## Semantics @@ -151,15 +176,6 @@ It might be desirable to use interfaces even when compiling "vo-style" rather th We speculate this can be accomplished by compiling `.vi` files to `.vos` outputs, and compiling `.v` files into `.vok` files. -== - -The goal of `.vi` files is to support separate compilation in Cardelli's sense: implementation changes that preserve the interface cannot affect clients. More formally, modules can be typechecked separately, and successful typechecking guarantees successful linking (again, up to universe checking; see below). For clarity, we intend "typechecking" to include all of elaboration, including the execution of proof scripts. If a client `bar.v` of a `foo.vi` interface elaborates correctly to a compiled file (`bar.vo` or `bar.vok`), and if `foo.v` satisfies its interface, - -The semantics of a `.vi` file would resemble today's opaque ascription with module types, while reducing boilerplate. Clients would only see the interface declared in the .vi file, but would not see the definitions of the .v file, nor its non-logical side effects such as hints. - -Unlike today, `.vi` interfaces would hide not just `Import`-bound side effects, but also `Require`-bound ones. [This might be kind-of possible today by hiding `Require` inside modules with opaque ascriptions, but `Require` is discouraged inside interactive modules.] - -A reviewer of our CoqPL paper objected to our proposal, because removing an interface file would reintroduce the hidden side effects and break clients. We consider this not a bug but a feature, essential to separate compilation: any change to the ### Universes @@ -182,7 +198,7 @@ A further issue is that universe inference does not seem to be prone to parallel ## Value -b.v` depends on `a.v`. Assume that `a.v` satisfies the interface in `a.vi` but adds universe constraints, and that `b.v` typechecks against `a.vi`. Moreover, assume that the universe constraints of `a.v` and `b.v` are both satisfiable in isolation. +`b.v` depends on `a.v`. Assume that `a.v` satisfies the interface in `a.vi` but adds universe constraints, and that `b.v` typechecks against `a.vi`. Moreover, assume that the universe constraints of `a.v` and `b.v` are both satisfiable in isolation. We have two problems: From cade9ed8c55a9f34cd81d1a333ebc42ea3c5ca9e Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Wed, 9 Feb 2022 21:37:52 -0500 Subject: [PATCH 04/30] Elaborating on the different possibilities. --- text/separate-compilation.md | 83 +++++++++++++++++++++--------------- 1 file changed, 48 insertions(+), 35 deletions(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 8a9a0a98..a01dbf19 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -8,7 +8,7 @@ Coq provides a module system that can be used explicitly through commands such a Avoiding dependencies that are only needed for non-exposed definitions, e.g. you do not need to expose the fact that proofs are constructed using particular tactics. Build parallelism (even without using -vos builds) because clients can be compiled against specification files only. -This CEP proposes several bits of sugar that makes it easier to use modules and achieve separate compilation. +This CEP proposes the introduction of a Coq interface file (which we will call a `.vi` file) that makes it possible to ascribe a `Moddule Type` to a top-level, i.e. declared as a file, `Module`. NOTE: In this proposal we use the extension `.vi` to be analog to `.mli` (derived from `.ml`). Similarly, we use `.vio` as what it compiles to. The `.vio` extension is already used for `-quick` build, so we could use `.vix` or anything else here. Or, remove `-quick` builds entirely and re-purpose the name. @@ -18,9 +18,16 @@ The goal of `.vi` files is to support separate compilation in Cardelli's sense: # Proposal -At the highest level, this proposal introduces the concept of an interface file with a `.vi` extension. An example of a `.vi` and `.v` file for a simple module would be the following: +This proposal introduces the concept of an interface file with a `.vi` extension. +We think of this file as containing the `Module Type` for the corresponding `.v` file (which contains the `Module` the way it currently does in Coq and Ocaml). +With the new file type, we have three situations to consider: both a `.vi` and a `.v` file, only a `.v` file, and only a `.vi** file. -``` +**Note**: In this section, we focus on the *Gallina*-level semantics focusing on the equivalent mathematical formulations. + +## Both a `.vi` and `.v` File +An example of a `.vi` and `.v` file for a simple module would be the following: + +```coq (* lib.vi *) Parameter value : nat. Axiom value_is_42 : value = 42. @@ -30,9 +37,9 @@ Definition value : nat := 42. Definition value_is_42 : value = 42 := ltac:(reflexivity). ``` -Conceptually, this pair of files could be compiled to the following single Coq file: +At the *Gallina*-level, this pair of files could be compiled to the following single Coq file: -``` +```coq (* lib_composed.v: *) Module Type LIB. Parameter value : nat. @@ -47,48 +54,54 @@ End lib. Export lib. (* make the declarations from lib available from [Import]ing lib (rather that lib.lib *) ``` -With the new file, there are two additional scenarios for considerations: - -1. A `.v` file without a `.vi` file. This *must not* change at all. It is analagous to having a `Module` without an opaque ascription. It is also equivalent to copy-pasting the `.v` file in the corresponding `.vi` file. [^vi-less] -2. A `.vi` file without a `.v` file. In this case, +Note that it is possible for `lib.vi` and `lib.v` to `Require` different libraries. +In this case, it is *crucial* that side-effects (e.g. definitions, tactics, hints, notations, etc) from the `.v` file are **not** visible by clients that `Require lib`. +Hiding these implementation details enables separate compilation, but the benefits go beyond build parallelism. -[^vi-less]: There is some disagreement here concerning whether the bodies of `Qed`d definitions should be included here. +## Only a `.v` File -/// REMOVE -if .vi is missing then - produce it by dropping the body of Qed definitions +It is crucial that having a `.v` file without a corresponding interface does *not* change the the current behavior of Coq. +In Gallina, this is analagous to having a `Module` without a `Module Type` ascription. -- after you do this, you only need to consider the .v&.vi case -* in the -vos build when you process a [Require] you get the .vio file -* in the vo build when you process the require, you read the .vio file and the .vo file pulling the universes from the later into the former +In order to provide a uniform semantic understanding, we opt to reduce this to the previous situation in which both files exist, but note explictly that an implementation may not do this. For example, in Ocaml, a single `.ml` file does *not* generate a `.cmi` file. -if the .vi is missing then - cp x.v x.vi -- after you do this, you only need to consider the .v&.vi case -* you read the information from .vio file, treat .vio as a .vo +The existance of dependent types and opaque definitions makes this question more subtle than the basic Ocaml solution. +We see three solutions: -vos, .vi -vos, .v -vos, .v{,i} -vo, .vi -vo, .v -vo, .v{,i} +1. *Verbatim* Synthesize the interface (the `.vi`) file using the *verbatim* contents of the `.v` file. This includes *all* definitions, hints, and other side effects. In particular it also includes the bodies of opaque (e.g. `Qed`d) defintions. While somewhat counter-intuitive, including the bodies of opaque definitions (as opposed to just their signature) means that we recover the exact semantics that we would get from including the implementation directly. +2. Synthesize the interface (the `.vi`) file using the contents of the `.v` file where opaque defintions (e.g. those that are `Qed`-d are replaced by `Parameter`s. There are two ways to do this: exactly and approximately. + - The *exact* characterization does not expose the body of the definition, but it does include its *full* characterization including universe constraints. Note that universe constraints may not be apparent from the type of the definition but they must still be included. + - The *approximate* characterization follows what a user would get from textually copying the type of the definition and converting it from a defined symbol to an assumed symbol, e.g. a `Parameter`. + + In this setup, the *exact* characterization is effectively the same as the first proposal, it simply changes the way that the opaque ascription is provided, i.e. from using `Qed` to using an opaque module ascription. + The *approximate* characterization follows (more closely) the semantics of `-vos` builds. This enables build parallelism at the cost of delayed universe checks (and all of the consequences of this). + +We note that both the *verbatim* proposal and the *exact* proposal are _effectively_ the same in the math. Aesthetically, we believe that the *exact* proposal seems cleaner, opting to hide more details from clients and use a more uniform sealing mechanism. The *Verbatim* option, on the other hand, seems more natural to understand and potentially implement. +## Only a `.vi` File -What are the build dependencies to build: client.v that requires lib. +When only an interface file exists, there is (potentially) no underlying implementation, but the existance of the interface should still provide definite references to an implementation. +Casting this in the feature set of the current Coq ecosystem, this essentially translates to a `Declare Module`. +Concretely, +```coq +(* lib.vi *) +Parameter answer : nat. +Axiom answer_is_42 : answer = 42. ``` -# full build with universe checking -lib.vio : lib.vo lib.vi -lib.vo : lib.v -# partial build (build speedup, no universe checking) -lib.vio : lib.vi -lib.vo : lib.vio lib.v +would be "translated" to: + +```coq +(* lib.v *) +Module Type LIB. + Parameter answer : nat. + Axiom answer_is_42 : answer = 42. +End LIB. -client.v : lib.vio +Declare Module lib : LIB. +Export lib. ``` -/// END REMOVE ## Semantics From b006139093d86cfafa13e706a2ff85d12ad94138 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Wed, 9 Feb 2022 21:50:58 -0500 Subject: [PATCH 05/30] Removing more duplication. --- text/separate-compilation.md | 34 ++++++++-------------------------- 1 file changed, 8 insertions(+), 26 deletions(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index a01dbf19..f06d5d99 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -8,7 +8,9 @@ Coq provides a module system that can be used explicitly through commands such a Avoiding dependencies that are only needed for non-exposed definitions, e.g. you do not need to expose the fact that proofs are constructed using particular tactics. Build parallelism (even without using -vos builds) because clients can be compiled against specification files only. -This CEP proposes the introduction of a Coq interface file (which we will call a `.vi` file) that makes it possible to ascribe a `Moddule Type` to a top-level, i.e. declared as a file, `Module`. +This CEP proposes the introduction of a Coq interface file (which we will call a `.vi` file) that makes it possible to ascribe a module type to a top-level, i.e. declared as a file, module. +The semantics of a `.vi` file would resemble today's opaque ascription with module types, while reducing boilerplate. Clients would only see the interface declared in the `.vi` file, but would neither see see the definitions of the `.v` file, nor its non-logical side effects such as hints. +Unlike today, `.vi` interfaces would hide not just `Import`-bound side effects, but also `Require`-bound ones. NOTE: In this proposal we use the extension `.vi` to be analog to `.mli` (derived from `.ml`). Similarly, we use `.vio` as what it compiles to. The `.vio` extension is already used for `-quick` build, so we could use `.vix` or anything else here. Or, remove `-quick` builds entirely and re-purpose the name. @@ -130,17 +132,14 @@ However, the extra universe constraints from `producer.vo` compared to `producer # Implementation -We speculate this can be accomplished by compiling `.vi` files to `.vos` outputs, and compiling `.v` files into `.vok` files. - -== - +The implementation would require (at least) the following: +1. Extending the build infrastructure to support `.vi` compilation. +2. Modifying the implementation of `Require` to search for `.vio` files in addition to `.vo` files. For backwards compatibility, we believe it would be important to search for both `.vio` and `.vo` files *simultaneously* rather than first searching for a `.vio` and then for a `.vo` because the later would mean that adding a `.vi` files could change the library that is used. +3. We believe that the bit-level representation of `.vio` could be the same as `.vo` files, though an alternative would be to leverage the representation of `.vos` files (which might be the same). -The semantics of a `.vi` file would resemble today's opaque ascription with module types, while reducing boilerplate. Clients would only see the interface declared in the .vi file, but would not see the definitions of the .v file, nor its non-logical side effects such as hints. - -Unlike today, `.vi` interfaces would hide not just `Import`-bound side effects, but also `Require`-bound ones. [This might be kind-of possible today by hiding `Require` inside modules with opaque ascriptions, but `Require` is discouraged inside interactive modules.] +== -A reviewer of our CoqPL paper objected to our proposal, because removing an interface file would reintroduce the hidden side effects and break clients. We consider this not a bug but a feature, essential to separate compilation: any change to the ### Universes @@ -153,15 +152,6 @@ To remedy this problem, we propose an additional "global" check. By analogy with Consider files `a.vi`, `a.v` and `b.v`, where `Title: Separate Compilation in Coq Authors: David Swasey, Paolo Giarrusso, Gregory Malecha` -# Summary - -Coq provides a module system that can be used explicitly through commands such as `Module` and `Module Type`. These can be quite heavyweight in many instances, and have some limitations when it comes to separately compiling files and building generic libraries. The ideas are drawn from OCaml, where .mli files can be used to express the interface of a module separately from its implementation. In addition to build parallelism, this also enables: -Avoiding dependencies that are only needed for non-exposed definitions, e.g. you do not need to expose the fact that proofs are constructed using particular tactics. -Build parallelism (even without using -vos builds) because clients can be compiled against specification files only. - -This CEP proposes several bits of sugar that makes it easier to use modules and achieve separate compilation. - - ## Semantics In this section we sketch the semantics informally — ignoring problems due to universe constraints until the relevant subsections. @@ -185,11 +175,6 @@ sometimes, Coq also seems to produce stricter universe constraints than strictly It might be desirable to use interfaces even when compiling "vo-style" rather than "vos-style". At least, it would be easier to check universes in such a mode. This means that compiling `consumer.v` would load `producer.vo` despite the existence of `producer.vi`. We propose that in this mode, most side effects of `producer.vo` shall be ignored anyway, including its `Require`-bound side effects. However, the extra universe constraints from `producer.vo` compared to `producer.vos` are important. -# Implementation - -We speculate this can be accomplished by compiling `.vi` files to `.vos` outputs, and compiling `.v` files into `.vok` files. - - ### Universes As some readers will anticipate, universe checks do not admit fully separate compilation; module bodies might add constraints absent from interfaces. This is already an issue with `.vos` builds today, and is a problem inherent to parallel builds, so any solutions to this problem could be shared. @@ -221,6 +206,3 @@ We can elaborate `a.v` and `b.v` separately, but their combination might produce A further issue is that universe inference does not seem to be prone to parallelism. Without seeing `producer.v`, -## Value - - From 648cec149baa4fd2b9777e5ca8cd7b8cd9ae770e Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Wed, 9 Feb 2022 21:56:09 -0500 Subject: [PATCH 06/30] Removing some more redundant text. --- text/separate-compilation.md | 36 ++++++------------------------------ 1 file changed, 6 insertions(+), 30 deletions(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index f06d5d99..6b9831d5 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -109,7 +109,7 @@ Export lib. In this section we sketch the semantics informally — ignoring problems due to universe constraints until the relevant subsections. -.vi interfaces are meant to hide implementations and support separate compilation in Cardelli's sense. Hence, a module `consumer.v` that consumes the interface of `producer.vi` shall be compiled without inspecting either `producer.v`, any build product from `producer.v`, or even the existence of `producer.v`. As a consequence, no change to `producer.v` can affect whether `consumer.v` typechecks. +`.vi` interfaces are meant to hide implementations and support separate compilation in Cardelli's sense. Hence, a module `consumer.v` that consumes the interface of `producer.vi` shall be compiled without inspecting either `producer.v`, any build product from `producer.v`, or even the existence of `producer.v`. As a consequence, no change to `producer.v` can affect whether `consumer.v` typechecks. Because Coq modules do not satisfy subsumption, removing `.vi` files can expose implementation details that break clients. This is a feature. @@ -149,18 +149,15 @@ We consider vos builds a special case of this proposal, where interfaces are inf To remedy this problem, we propose an additional "global" check. By analogy with separate compilation in other languages, we call this "link-time" universe checking. -Consider files `a.vi`, `a.v` and `b.v`, where `Title: Separate Compilation in Coq -Authors: David Swasey, Paolo Giarrusso, Gregory Malecha` - -## Semantics +Consider files `a.vi`, `a.v` and `b.v`, where `b.v` depends on `a.v`. Assume that `a.v` satisfies the interface in `a.vi` but adds universe constraints, and that `b.v` typechecks against `a.vi`. Moreover, assume that the universe constraints of `a.v` and `b.v` are both satisfiable in isolation. -In this section we sketch the semantics informally — ignoring problems due to universe constraints until the relevant subsections. +We have two problems: -.vi interfaces are meant to hide implementations and support separate compilation in Cardelli's sense. Hence, a module `consumer.v` that consumes the interface of `producer.vi` shall be compiled without inspecting either `producer.v`, any build product from `producer.v`, or even the existence of `producer.v`. As a consequence, no change to `producer.v` can affect whether `consumer.v` typechecks. +Composing the universe constraints of `a.v` and `b.v` might produce an unsatisfiable constraint set, but this is not detected. This can also +We can elaborate `a.v` and `b.v` separately, but their combination might produce an unsatisfiable -Because Coq modules do not satisfy subsumption, removing `.vi` files can expose implementation details that break clients. This is a feature. -`.vi` interfaces can hide `Require`-bound side effects. Hiding is also an intentional feature, that is supported automatically in the above compilation model. However, this feature is not supported today, either via existing `vos` builds or via opaque ascription. [One can write a Require in an interactive module, but Coq complains enough we have not explored what happens. If we lift the Require out into the surrounding top-level module, its side effects cannot be hidden.] +A further issue is that universe inference does not seem to be prone to parallelism. Without seeing `producer.v`, ### "Link-time" Universe Checking @@ -171,27 +168,6 @@ The above assumes that universes and universe constraints for a term can be gene for instance, some Ltac can fail with an universe inconsistency and backtrack (as mentioned in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/vos.2Fvok.20and.20link-time.20universe.20check); we propose that the extra constraints be hidden at this stage sometimes, Coq also seems to produce stricter universe constraints than strictly needed, as Gaëtan shows in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Why.20does.20my.20fix.20for.20a.20universe.20problem.20work.3F/near/264903292. It'd be nice if the constraints were produced modularly, even if this might produce bigger graphs (hopefully in a tolerable way), or might require manual eta-expansion (we'd need Coq to give a warning/error when it must eta-expand, suggesting the user do that by hand). -### "Full compilation" semantics - -It might be desirable to use interfaces even when compiling "vo-style" rather than "vos-style". At least, it would be easier to check universes in such a mode. This means that compiling `consumer.v` would load `producer.vo` despite the existence of `producer.vi`. We propose that in this mode, most side effects of `producer.vo` shall be ignored anyway, including its `Require`-bound side effects. However, the extra universe constraints from `producer.vo` compared to `producer.vos` are important. - -### Universes - -As some readers will anticipate, universe checks do not admit fully separate compilation; module bodies might add constraints absent from interfaces. This is already an issue with `.vos` builds today, and is a problem inherent to parallel builds, so any solutions to this problem could be shared. - -We consider vos builds a special case of this proposal, where interfaces are inferred as the strictest possible ones for the given implementation; `.vi` files enable hiding more implementation details. In both cases, the interface omits universe constraints that are derived from hidden bodies (for vos builds, just Qed bodies). While some universe checks are performed anyway, omitted constraints might make the universe graph unsatisfiable. - -To remedy this problem, we propose an additional "global" check. By analogy with separate compilation in other languages, we call this "link-time" universe checking. - -Consider files `a.vi`, `a.v` and `b.v`, where `b.v` depends on `a.v`. Assume that `a.v` satisfies the interface in `a.vi` but adds universe constraints, and that `b.v` typechecks against `a.vi`. Moreover, assume that the universe constraints of `a.v` and `b.v` are both satisfiable in isolation. - -We have two problems: - -Composing the universe constraints of `a.v` and `b.v` might produce an unsatisfiable constraint set, but this is not detected. This can also -We can elaborate `a.v` and `b.v` separately, but their combination might produce an unsatisfiable - - -A further issue is that universe inference does not seem to be prone to parallelism. Without seeing `producer.v`, ## Value From 0d29e794f7f0fae7c370cc7883b51ece4aefe4d2 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Wed, 9 Feb 2022 22:16:02 -0500 Subject: [PATCH 07/30] More consolidation. --- text/separate-compilation.md | 76 ++++++++++-------------------------- 1 file changed, 21 insertions(+), 55 deletions(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 6b9831d5..d732c55f 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -22,9 +22,14 @@ The goal of `.vi` files is to support separate compilation in Cardelli's sense: This proposal introduces the concept of an interface file with a `.vi` extension. We think of this file as containing the `Module Type` for the corresponding `.v` file (which contains the `Module` the way it currently does in Coq and Ocaml). -With the new file type, we have three situations to consider: both a `.vi` and a `.v` file, only a `.v` file, and only a `.vi** file. +`.vi` interfaces are meant to hide implementations and support separate compilation in Cardelli's sense. Hence, a module `consumer.v` that consumes the interface of `producer.vi` shall be compiled without inspecting either `producer.v`, any build product from `producer.v`, or even the existence of `producer.v`. As a consequence, no change to `producer.v** can affect whether `consumer.v** typechecks. + +**Caveat** Because the behavior of Coq (e.g. tactics), as opposed to Gallina, can change when more definitions become available, removing a `.vi` file can expose implementation details that break client proof scripts though (we believe) that it can not break kernel type checking in theory (i.e. ignoring practical considerations such as conversion times). We consider the potential to break clients a feature because meta-reasoning *should* occur at the interface and note the implemenation. -**Note**: In this section, we focus on the *Gallina*-level semantics focusing on the equivalent mathematical formulations. +In this section, we focus on the *Gallina*-level semantics focusing on the equivalent mathematical formulations. +We delay consideration of universes until the relevant subsection. + +With the new file type, we have three situations to consider: both a `.vi` and a `.v` file, only a `.v` file, and only a `.vi** file. ## Both a `.vi` and `.v` File An example of a `.vi` and `.v` file for a simple module would be the following: @@ -105,43 +110,7 @@ Declare Module lib : LIB. Export lib. ``` -## Semantics - -In this section we sketch the semantics informally — ignoring problems due to universe constraints until the relevant subsections. - -`.vi` interfaces are meant to hide implementations and support separate compilation in Cardelli's sense. Hence, a module `consumer.v` that consumes the interface of `producer.vi` shall be compiled without inspecting either `producer.v`, any build product from `producer.v`, or even the existence of `producer.v`. As a consequence, no change to `producer.v` can affect whether `consumer.v` typechecks. - -Because Coq modules do not satisfy subsumption, removing `.vi` files can expose implementation details that break clients. This is a feature. - -`.vi` interfaces can hide `Require`-bound side effects. Hiding is also an intentional feature, that is supported automatically in the above compilation model. However, this feature is not supported today, either via existing `vos` builds or via opaque ascription. [One can write a Require in an interactive module, but Coq complains enough we have not explored what happens. If we lift the Require out into the surrounding top-level module, its side effects cannot be hidden.] - -### "Link-time" Universe Checking - -Cardelli's separate compilation has a further demand: in this example, if `consumer.v` typechecks, and `producer.v` satisfies its interface, the two shall link successfully. In Coq this is true except for universe constraints, like for existing `.vos` builds. To alleviate this problem, we propose -extending `.vok` outputs to include proof terms, or at least universe constraints -so that we can run a "link-time checker" that loads the whole program and checks whether combined universe constraints are satisfiable. -The above assumes that universes and universe constraints for a term can be generated in isolation. However, universe inference is sometimes too greedy: when compiling `consumer.v` without the universe constraints from `producer.v`, Coq will sometimes produce different terms. -for instance, some Ltac can fail with an universe inconsistency and backtrack (as mentioned in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/vos.2Fvok.20and.20link-time.20universe.20check); we propose that the extra constraints be hidden at this stage -sometimes, Coq also seems to produce stricter universe constraints than strictly needed, as Gaëtan shows in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Why.20does.20my.20fix.20for.20a.20universe.20problem.20work.3F/near/264903292. It'd be nice if the constraints were produced modularly, even if this might produce bigger graphs (hopefully in a tolerable way), or might require manual eta-expansion (we'd need Coq to give a warning/error when it must eta-expand, suggesting the user do that by hand). - -### "Full compilation" semantics - -It might be desirable to use interfaces even when compiling "vo-style" rather than "vos-style". At least, it would be easier to check universes in such a mode. -This means that compiling `consumer.v` would load `producer.vo` despite the existence of `producer.vi`. We propose that in this mode, most side effects of `producer.vo` shall be ignored anyway, including its `Require`-bound side effects. -However, the extra universe constraints from `producer.vo` compared to `producer.vos` are important. - -# Implementation - -The implementation would require (at least) the following: - -1. Extending the build infrastructure to support `.vi` compilation. -2. Modifying the implementation of `Require` to search for `.vio` files in addition to `.vo` files. For backwards compatibility, we believe it would be important to search for both `.vio` and `.vo` files *simultaneously* rather than first searching for a `.vio` and then for a `.vo` because the later would mean that adding a `.vi` files could change the library that is used. -3. We believe that the bit-level representation of `.vio` could be the same as `.vo` files, though an alternative would be to leverage the representation of `.vos` files (which might be the same). - -== - - -### Universes +## Universes As some readers will anticipate, universe checks do not admit fully separate compilation; module bodies might add constraints absent from interfaces. This is already an issue with `.vos` builds today, and is a problem inherent to parallel builds, so any solutions to this problem could be shared. @@ -153,32 +122,29 @@ Consider files `a.vi`, `a.v` and `b.v`, where `b.v` depends on `a.v`. Assume tha We have two problems: -Composing the universe constraints of `a.v` and `b.v` might produce an unsatisfiable constraint set, but this is not detected. This can also -We can elaborate `a.v` and `b.v` separately, but their combination might produce an unsatisfiable - +1. Composing the universe constraints of `a.v` and `b.v` might produce an unsatisfiable constraint set, but this is not detected. This can also occur in "vos-style" builds. +2. We can elaborate `a.v` and `b.v` separately, but their combination might produce an unsatisfiable universe graph. A further issue is that universe inference does not seem to be prone to parallelism. Without seeing `producer.v`, -### "Link-time" Universe Checking -Cardelli's separate compilation has a further demand: in this example, if `consumer.v` typechecks, and `producer.v` satisfies its interface, the two shall link successfully. In Coq this is true except for universe constraints, like for existing `.vos` builds. To alleviate this problem, we propose -extending `.vok` outputs to include proof terms, or at least universe constraints -so that we can run a "link-time checker" that loads the whole program and checks whether combined universe constraints are satisfiable. -The above assumes that universes and universe constraints for a term can be generated in isolation. However, universe inference is sometimes too greedy: when compiling `consumer.v` without the universe constraints from `producer.v`, Coq will sometimes produce different terms. -for instance, some Ltac can fail with an universe inconsistency and backtrack (as mentioned in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/vos.2Fvok.20and.20link-time.20universe.20check); we propose that the extra constraints be hidden at this stage -sometimes, Coq also seems to produce stricter universe constraints than strictly needed, as Gaëtan shows in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Why.20does.20my.20fix.20for.20a.20universe.20problem.20work.3F/near/264903292. It'd be nice if the constraints were produced modularly, even if this might produce bigger graphs (hopefully in a tolerable way), or might require manual eta-expansion (we'd need Coq to give a warning/error when it must eta-expand, suggesting the user do that by hand). +### "Link-time" Universe Checking +Cardelli's separate compilation has a further demand: in this example, if `consumer.v` typechecks, and `producer.v` satisfies its interface, the two shall link successfully. In Coq this is true except for universe constraints, like for existing `.vos` builds. To alleviate this problem, we propos`extending `.vok` outputs to i`lude proof terms, or at least universe constraint`so that we can r` a "link-time checker" that loads the whole program and checks whether combined universe constraints are satisfiable`The above assumes that u`verses and universe constraints for a term can be generated in isolation. However, universe inference is sometimes too greedy: when compiling `consumer.v` without the universe constraints from `producer.v`, Coq will sometimes produce different terms`for instance, some Ltac c` fail with an universe inconsistency and backtrack (as mentioned in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/vos.2Fvok.20and.20link-time.20universe.20check); we propose that the extra constraints be hidden at this stag`sometimes, Coq also seems t`produce stricter universe constraints than strictly needed, as Gaëtan shows in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Why.20does.20my.20fix.20for.20a.20universe.20problem.20work.3F/near/264903292. It'd be nice if the constraints were produced modularly, even if this might produce bigger graphs (hopefully in a tolerable way), or might require manual eta-expansion (we'd need Coq to give a warning/error when it must eta-expand, suggesting the user do that by hand)` -## Value +### "Full compilation" semantics +The notion of full compilation semantics, i.e. a sound full-build semantics akin to a "vo-style" build can be achieved (at the cost of build parallelism) by introducing a dependency between the `.vio` file and the `.vo` file and elaboring the resulting `.vio` file with universe constraints introduced by the implementation. It is important that this does not include other side-effects from the `.vo` such as hints, tactics, or plugin requirements. -`b.v` depends on `a.v`. Assume that `a.v` satisfies the interface in `a.vi` but adds universe constraints, and that `b.v` typechecks against `a.vi`. Moreover, assume that the universe constraints of `a.v` and `b.v` are both satisfiable in isolation. -We have two problems: +[//]: # It might be desirable to use interfaces even when compiling "vo-style" rather than "vos-style". At least, it would be easier to check universes in such a mode. This means that compiling `consumer.v` would load `producer.vo` despite the existence of `producer.vi`. We propose that in this mode, most side effects of `producer.vo` shall be ignored anyway, including its `Require`-bound side effects. +However, the extra universe constraints from `producer.vo` compared to `producer.vos` are important. -Composing the universe constraints of `a.v` and `b.v` might produce an unsatisfiable constraint set, but this is not detected. This can also -We can elaborate `a.v` and `b.v` separately, but their combination might produce an unsatisfiable +# Implementation +The implementation would require (at least) the following: -A further issue is that universe inference does not seem to be prone to parallelism. Without seeing `producer.v`, +1. Extending the build infrastructure to support `.vi` compilation. +2. Modifying the implementation of `Require` to search for `.vio` files in addition to `.vo` files. For backwards compatibility, we believe it would be important to search for both `.vio` and `.vo` files *simultaneously* rather than first searching for a `.vio` and then for a `.vo` because the later would mean that adding a `.vi` files could change the library that is used. +3. We believe that the bit-level representation of `.vio` could be the same as `.vo` files, though an alternative would be to leverage the representation of `.vos` files (which might be the same). From ec81a87d6975e7b5d9b1e2154a2971f6ff4cc966 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Wed, 9 Feb 2022 22:19:40 -0500 Subject: [PATCH 08/30] A note about full functorization (though it might be off-topic). --- text/separate-compilation.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index d732c55f..35c21c81 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -88,7 +88,7 @@ We note that both the *verbatim* proposal and the *exact* proposal are _effectiv ## Only a `.vi` File When only an interface file exists, there is (potentially) no underlying implementation, but the existance of the interface should still provide definite references to an implementation. -Casting this in the feature set of the current Coq ecosystem, this essentially translates to a `Declare Module`. +Casting this in the feature set of the current Coq ecosystem, this essentially translates to a `Declare Module` [^full-functorization]. Concretely, ```coq @@ -148,3 +148,4 @@ The implementation would require (at least) the following: 2. Modifying the implementation of `Require` to search for `.vio` files in addition to `.vo` files. For backwards compatibility, we believe it would be important to search for both `.vio` and `.vo` files *simultaneously* rather than first searching for a `.vio` and then for a `.vo` because the later would mean that adding a `.vi` files could change the library that is used. 3. We believe that the bit-level representation of `.vio` could be the same as `.vo` files, though an alternative would be to leverage the representation of `.vos` files (which might be the same). +[^full-functorization]: An alternative characterization of `Declare Module` is to implicitly functorize all dependent modules over the module type of the declared module. This understanding of `Declare Module` does enable some additional flexibility at "link-time" but is beyond the scope of this proposal. From 2b15916c7edb0914a5ba0a6e629957534eb26a33 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sat, 12 Feb 2022 22:11:00 +0100 Subject: [PATCH 09/30] Summary: significant revision/rewrite This rewrite preserves most of the old content, but I hope it flows better and is more obviously compelling. --- text/separate-compilation.md | 41 ++++++++++++++++++++++++++++-------- 1 file changed, 32 insertions(+), 9 deletions(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 35c21c81..c2c44cdf 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -4,15 +4,38 @@ # Summary -Coq provides a module system that can be used explicitly through commands such as `Module` and `Module Type`. These can be quite heavyweight in many instances, and have some limitations when it comes to separately compiling files and building generic libraries. The ideas are drawn from OCaml, where .mli files can be used to express the interface of a module separately from its implementation. This enables: -Avoiding dependencies that are only needed for non-exposed definitions, e.g. you do not need to expose the fact that proofs are constructed using particular tactics. -Build parallelism (even without using -vos builds) because clients can be compiled against specification files only. - -This CEP proposes the introduction of a Coq interface file (which we will call a `.vi` file) that makes it possible to ascribe a module type to a top-level, i.e. declared as a file, module. -The semantics of a `.vi` file would resemble today's opaque ascription with module types, while reducing boilerplate. Clients would only see the interface declared in the `.vi` file, but would neither see see the definitions of the `.v` file, nor its non-logical side effects such as hints. -Unlike today, `.vi` interfaces would hide not just `Import`-bound side effects, but also `Require`-bound ones. - -NOTE: In this proposal we use the extension `.vi` to be analog to `.mli` (derived from `.ml`). Similarly, we use `.vio` as what it compiles to. The `.vio` extension is already used for `-quick` build, so we could use `.vix` or anything else here. Or, remove `-quick` builds entirely and re-purpose the name. +Coq provides a module system that can be used explicitly through commands such +as `Module` and `Module Type`. These can be quite heavyweight in many instances, +and have some limitations when it comes to separately compiling files and +building generic libraries. +To address these problems, and support information hiding and separate +compilation, in this CEP we introduce a notion of Coq interface files, which we +will call a `.vi` file, and which are inspired by OCaml's `.mli` files. +Intuitively, a Coq interface file called `module.vi` defines the public +interface for `module.v`. The `module.vi` interface shall enable developing and +typechecking clients, even before `module.v` has been implemented. + +If both `module.vi` and `module.v` are present, `module.vi` shall act as an +opaque ascription for the top-level module defined by `module.v`; this opaque +ascription ensures that clients that typecheck against `module.vi` shall still +typecheck against the combination of `module.vi` and `module.v`, regardless of +the implementation details of `module.v`, including any non-logical side effects +such as hints. +(except for universe constraints, as we discuss later). + +This has a few advantages: +- it enables separate development: after agreeing `module.vi`, `module.v` and + its clients can be developed independently. To ensure this, unlike today's + opaque ascription, `.vi` files can even hide side effects due to `Require`. +- it reduces compile-time dependencies and improves compile times, even compared + to today's `vos` builds (initial builds can be more parallel, and incremental + builds need to recompile fewer files). + +NOTE: For concreteness, in this CEP we use the `.vi` extension for for interface +source files, and the `.vio` extension for interface object files. However, +`.vio` files should not be confused with `.vio` files produced by `-quick` +builds: to avoid confusion, we could choose other file extensions or remove +`-quick` builds entirely. ## Background From 965951023a6ed9390da2668e74699d4cdd24261b Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sat, 12 Feb 2022 22:14:00 +0100 Subject: [PATCH 10/30] can not -> cannot --- text/separate-compilation.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index c2c44cdf..0e2bd674 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -47,7 +47,7 @@ This proposal introduces the concept of an interface file with a `.vi` extension We think of this file as containing the `Module Type` for the corresponding `.v` file (which contains the `Module` the way it currently does in Coq and Ocaml). `.vi` interfaces are meant to hide implementations and support separate compilation in Cardelli's sense. Hence, a module `consumer.v` that consumes the interface of `producer.vi` shall be compiled without inspecting either `producer.v`, any build product from `producer.v`, or even the existence of `producer.v`. As a consequence, no change to `producer.v** can affect whether `consumer.v** typechecks. -**Caveat** Because the behavior of Coq (e.g. tactics), as opposed to Gallina, can change when more definitions become available, removing a `.vi` file can expose implementation details that break client proof scripts though (we believe) that it can not break kernel type checking in theory (i.e. ignoring practical considerations such as conversion times). We consider the potential to break clients a feature because meta-reasoning *should* occur at the interface and note the implemenation. +**Caveat** Because the behavior of Coq (e.g. tactics), as opposed to Gallina, can change when more definitions become available, removing a `.vi` file can expose implementation details that break client proof scripts though (we believe) that it cannot break kernel type checking in theory (i.e. ignoring practical considerations such as conversion times). We consider the potential to break clients a feature because meta-reasoning *should* occur at the interface and note the implemenation. In this section, we focus on the *Gallina*-level semantics focusing on the equivalent mathematical formulations. We delay consideration of universes until the relevant subsection. From 15fb9b3040bde6f194a3acac25a32cebb9677e8c Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sat, 12 Feb 2022 23:38:20 +0100 Subject: [PATCH 11/30] Other typos --- text/separate-compilation.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 0e2bd674..a8dce4f2 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -47,12 +47,12 @@ This proposal introduces the concept of an interface file with a `.vi` extension We think of this file as containing the `Module Type` for the corresponding `.v` file (which contains the `Module` the way it currently does in Coq and Ocaml). `.vi` interfaces are meant to hide implementations and support separate compilation in Cardelli's sense. Hence, a module `consumer.v` that consumes the interface of `producer.vi` shall be compiled without inspecting either `producer.v`, any build product from `producer.v`, or even the existence of `producer.v`. As a consequence, no change to `producer.v** can affect whether `consumer.v** typechecks. -**Caveat** Because the behavior of Coq (e.g. tactics), as opposed to Gallina, can change when more definitions become available, removing a `.vi` file can expose implementation details that break client proof scripts though (we believe) that it cannot break kernel type checking in theory (i.e. ignoring practical considerations such as conversion times). We consider the potential to break clients a feature because meta-reasoning *should* occur at the interface and note the implemenation. +**Caveat** Because the behavior of Coq (e.g. tactics), as opposed to Gallina, can change when more definitions become available, removing a `.vi` file can expose implementation details that break client proof scripts though (we believe) that it cannot break kernel type checking in theory (i.e. ignoring practical considerations such as conversion times). We consider the potential to break clients a feature because meta-reasoning *should* occur at the interface and not the implemenation. In this section, we focus on the *Gallina*-level semantics focusing on the equivalent mathematical formulations. We delay consideration of universes until the relevant subsection. -With the new file type, we have three situations to consider: both a `.vi` and a `.v` file, only a `.v` file, and only a `.vi** file. +With the new file type, we have three situations to consider: both a `.vi` and a `.v` file, only a `.v` file, and only a `.vi` file. ## Both a `.vi` and `.v` File An example of a `.vi` and `.v` file for a simple module would be the following: From aacf72a3dec749992c23797502cea715088fa9a6 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sat, 12 Feb 2022 23:38:27 +0100 Subject: [PATCH 12/30] Drop my old background (now covered in intro) --- text/separate-compilation.md | 4 ---- 1 file changed, 4 deletions(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index a8dce4f2..7c10f434 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -37,10 +37,6 @@ source files, and the `.vio` extension for interface object files. However, builds: to avoid confusion, we could choose other file extensions or remove `-quick` builds entirely. -## Background - -The goal of `.vi` files is to support separate compilation in Cardelli's sense: implementation changes that preserve the interface cannot affect clients. More formally, modules can be typechecked separately, and successful typechecking guarantees successful linking (again, up to universe checking; see below). For clarity, we intend "typechecking" to include all of elaboration, including the execution of proof scripts. If a client `bar.v` of a `foo.vi` interface elaborates correctly to a compiled file (`bar.vo` or `bar.vok`), and if `foo.v` satisfies its interface, - # Proposal This proposal introduces the concept of an interface file with a `.vi` extension. From aeb21f71f683b19530263ab06a7ac9f5c7446679 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sat, 12 Feb 2022 23:53:15 +0100 Subject: [PATCH 13/30] Intro tweaks --- text/separate-compilation.md | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 7c10f434..0fcfac42 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -8,7 +8,7 @@ Coq provides a module system that can be used explicitly through commands such as `Module` and `Module Type`. These can be quite heavyweight in many instances, and have some limitations when it comes to separately compiling files and building generic libraries. -To address these problems, and support information hiding and separate +To address these problems, and support information hiding and Cardelli-style separate compilation, in this CEP we introduce a notion of Coq interface files, which we will call a `.vi` file, and which are inspired by OCaml's `.mli` files. Intuitively, a Coq interface file called `module.vi` defines the public @@ -19,15 +19,14 @@ If both `module.vi` and `module.v` are present, `module.vi` shall act as an opaque ascription for the top-level module defined by `module.v`; this opaque ascription ensures that clients that typecheck against `module.vi` shall still typecheck against the combination of `module.vi` and `module.v`, regardless of -the implementation details of `module.v`, including any non-logical side effects -such as hints. -(except for universe constraints, as we discuss later). +the implementation details of `module.v`,[^intro-universes] including any +non-logical side effects such as hints (but excluding [universes](#universes)). -This has a few advantages: -- it enables separate development: after agreeing `module.vi`, `module.v` and +This has a few advantages compared to Coq's state of the art: +- It enables separate development: after agreeing `module.vi`, `module.v` and its clients can be developed independently. To ensure this, unlike today's opaque ascription, `.vi` files can even hide side effects due to `Require`. -- it reduces compile-time dependencies and improves compile times, even compared +- It reduces compile-time dependencies and improves compile times, even compared to today's `vos` builds (initial builds can be more parallel, and incremental builds need to recompile fewer files). From 6bfae811752638edcc1c16ec670b4d838d6299b2 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 13 Feb 2022 00:02:09 +0100 Subject: [PATCH 14/30] Reinforce (indirectly) that interfaces affect compilation --- text/separate-compilation.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 0fcfac42..1941ca33 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -21,6 +21,9 @@ ascription ensures that clients that typecheck against `module.vi` shall still typecheck against the combination of `module.vi` and `module.v`, regardless of the implementation details of `module.v`,[^intro-universes] including any non-logical side effects such as hints (but excluding [universes](#universes)). +Instead, without interfaces, adding implementations is sufficient to break +clients, and changing implementations can break clients again, hindering modular +development. This has a few advantages compared to Coq's state of the art: - It enables separate development: after agreeing `module.vi`, `module.v` and From 0e2c2a1a5b4aa158d11424995a451e20cc30e15e Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 13 Feb 2022 00:09:39 +0100 Subject: [PATCH 15/30] Remove caveat: addressed earlier indirectly Yes, a reviewer asked specifically, but this caveat is awkward and the point should be clearer from the rest of the document. --- text/separate-compilation.md | 1 - 1 file changed, 1 deletion(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 1941ca33..0dedfde4 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -45,7 +45,6 @@ This proposal introduces the concept of an interface file with a `.vi` extension We think of this file as containing the `Module Type` for the corresponding `.v` file (which contains the `Module` the way it currently does in Coq and Ocaml). `.vi` interfaces are meant to hide implementations and support separate compilation in Cardelli's sense. Hence, a module `consumer.v` that consumes the interface of `producer.vi` shall be compiled without inspecting either `producer.v`, any build product from `producer.v`, or even the existence of `producer.v`. As a consequence, no change to `producer.v** can affect whether `consumer.v** typechecks. -**Caveat** Because the behavior of Coq (e.g. tactics), as opposed to Gallina, can change when more definitions become available, removing a `.vi` file can expose implementation details that break client proof scripts though (we believe) that it cannot break kernel type checking in theory (i.e. ignoring practical considerations such as conversion times). We consider the potential to break clients a feature because meta-reasoning *should* occur at the interface and not the implemenation. In this section, we focus on the *Gallina*-level semantics focusing on the equivalent mathematical formulations. We delay consideration of universes until the relevant subsection. From 50bcff89e906adbcf4e8028bf4be27fdee43d4be Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 13 Feb 2022 00:10:58 +0100 Subject: [PATCH 16/30] Revise section titles --- text/separate-compilation.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 0dedfde4..7051781e 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -39,7 +39,7 @@ source files, and the `.vio` extension for interface object files. However, builds: to avoid confusion, we could choose other file extensions or remove `-quick` builds entirely. -# Proposal +# Proposed Semantics This proposal introduces the concept of an interface file with a `.vi` extension. We think of this file as containing the `Module Type` for the corresponding `.v` file (which contains the `Module` the way it currently does in Coq and Ocaml). @@ -152,7 +152,7 @@ A further issue is that universe inference does not seem to be prone to parallel Cardelli's separate compilation has a further demand: in this example, if `consumer.v` typechecks, and `producer.v` satisfies its interface, the two shall link successfully. In Coq this is true except for universe constraints, like for existing `.vos` builds. To alleviate this problem, we propos`extending `.vok` outputs to i`lude proof terms, or at least universe constraint`so that we can r` a "link-time checker" that loads the whole program and checks whether combined universe constraints are satisfiable`The above assumes that u`verses and universe constraints for a term can be generated in isolation. However, universe inference is sometimes too greedy: when compiling `consumer.v` without the universe constraints from `producer.v`, Coq will sometimes produce different terms`for instance, some Ltac c` fail with an universe inconsistency and backtrack (as mentioned in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/vos.2Fvok.20and.20link-time.20universe.20check); we propose that the extra constraints be hidden at this stag`sometimes, Coq also seems t`produce stricter universe constraints than strictly needed, as Gaëtan shows in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Why.20does.20my.20fix.20for.20a.20universe.20problem.20work.3F/near/264903292. It'd be nice if the constraints were produced modularly, even if this might produce bigger graphs (hopefully in a tolerable way), or might require manual eta-expansion (we'd need Coq to give a warning/error when it must eta-expand, suggesting the user do that by hand)` -### "Full compilation" semantics +### "Full compilation" Semantics The notion of full compilation semantics, i.e. a sound full-build semantics akin to a "vo-style" build can be achieved (at the cost of build parallelism) by introducing a dependency between the `.vio` file and the `.vo` file and elaboring the resulting `.vio` file with universe constraints introduced by the implementation. It is important that this does not include other side-effects from the `.vo` such as hints, tactics, or plugin requirements. From 8882a741913800fb1ebabb145a571acea4b2f371 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 13 Feb 2022 00:18:06 +0100 Subject: [PATCH 17/30] Section 2: restructure/reflow --- text/separate-compilation.md | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 7051781e..4e725114 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -41,15 +41,17 @@ builds: to avoid confusion, we could choose other file extensions or remove # Proposed Semantics -This proposal introduces the concept of an interface file with a `.vi` extension. -We think of this file as containing the `Module Type` for the corresponding `.v` file (which contains the `Module` the way it currently does in Coq and Ocaml). -`.vi` interfaces are meant to hide implementations and support separate compilation in Cardelli's sense. Hence, a module `consumer.v` that consumes the interface of `producer.vi` shall be compiled without inspecting either `producer.v`, any build product from `producer.v`, or even the existence of `producer.v`. As a consequence, no change to `producer.v** can affect whether `consumer.v** typechecks. +In this section, we describe the meaning of our Coq extension: instead of +suggesting an implementation strategy, we sketch a *Gallina*-level +semantics, to be taken as an informal specification. +As a key principle: `.vi` interfaces are meant to hide implementations and support separate compilation in Cardelli's sense. Hence, compiling a module `consumer.v` that consumes the interface of `producer.vi` shall not depend (directly or indirectly) on the existence of `producer.v` or its contents. As a consequence, no change to `producer.v` can affect whether `consumer.v` typechecks. -In this section, we focus on the *Gallina*-level semantics focusing on the equivalent mathematical formulations. -We delay consideration of universes until the relevant subsection. - -With the new file type, we have three situations to consider: both a `.vi` and a `.v` file, only a `.v` file, and only a `.vi` file. +More concretely, our semantics for compiling top-level module (say, `lib`) +distinguishes three scenarios, depending on the existence of: +- both `lib.vi` and `lib.v`; +- only `lib.v`; +- or only `lib.vi`. ## Both a `.vi` and `.v` File An example of a `.vi` and `.v` file for a simple module would be the following: From 28cacc9797196476f7eb8a64f78b947fcae0d19f Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 13 Feb 2022 00:56:11 +0100 Subject: [PATCH 18/30] Both `.vi` and `.v`: significant revisions, demonstrate impl.-only requires, ... --- text/separate-compilation.md | 56 ++++++++++++++++++++++++++---------- 1 file changed, 41 insertions(+), 15 deletions(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 4e725114..1bc859ea 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -42,8 +42,10 @@ builds: to avoid confusion, we could choose other file extensions or remove # Proposed Semantics In this section, we describe the meaning of our Coq extension: instead of -suggesting an implementation strategy, we sketch a *Gallina*-level -semantics, to be taken as an informal specification. +suggesting an implementation strategy, we sketch a semantics as a +source-to-source transformation, to be taken as an informal and _approximate_ +specification. However, this is an approximate specification, because the exact +semantics cannot be expressed via source-to-source transformation. As a key principle: `.vi` interfaces are meant to hide implementations and support separate compilation in Cardelli's sense. Hence, compiling a module `consumer.v` that consumes the interface of `producer.vi` shall not depend (directly or indirectly) on the existence of `producer.v` or its contents. As a consequence, no change to `producer.v` can affect whether `consumer.v` typechecks. @@ -54,38 +56,62 @@ distinguishes three scenarios, depending on the existence of: - or only `lib.vi`. ## Both a `.vi` and `.v` File -An example of a `.vi` and `.v` file for a simple module would be the following: + +For concreteness, consider the following example: ```coq (* lib.vi *) +Global Open Scope Z_scope. Parameter value : nat. -Axiom value_is_42 : value = 42. +Axiom value_is_42 : value = 42%nat. (* lib.v *) +Require Import stdpp.prelude. +Global Open Scope N_scope. + Definition value : nat := 42. -Definition value_is_42 : value = 42 := ltac:(reflexivity). +Definition value_is_42 : value = 42%nat := ltac:(reflexivity). + +Definition other_value : N := 42. ``` -At the *Gallina*-level, this pair of files could be compiled to the following single Coq file: +Here, `lib.v` contains both the implementation of `lib.vi` and some commands +that perform global side effects and that should be hidden from clients: +`stdpp.prelude` modifies many Coq settings aggressively, even when simply +`Require`d, so adding this `Require` is a significant breaking change. + +In this example, the semantics of `lib` would resemble the semantics of the +following Coq source: ```coq (* lib_composed.v: *) -Module Type LIB. +Module Type __LIB. + Global Open Scope Z_scope. Parameter value : nat. Axiom value_is_42 : value = 42. -End LIB. +End __LIB. + +Module __lib : __LIB. + Require Import stdpp.prelude. + Global Open Scope N_scope. -Module lib : LIB. Definition value : nat := 42. - Definition value_is_42 : value = 42 := ltac:(reflexivity). -End lib. + Definition value_is_42 : value = 42%nat := ltac:(reflexivity). +End __lib. -Export lib. (* make the declarations from lib available from [Import]ing lib (rather that lib.lib *) +Export __lib. (* make the declarations from lib available from [Import]ing lib (rather that lib.lib *) ``` -Note that it is possible for `lib.vi` and `lib.v` to `Require` different libraries. -In this case, it is *crucial* that side-effects (e.g. definitions, tactics, hints, notations, etc) from the `.v` file are **not** visible by clients that `Require lib`. -Hiding these implementation details enables separate compilation, but the benefits go beyond build parallelism. +In this example translation, we use the `\_\_` prefix for generated identifiers +used as a translation device; these identifiers should be hidden from clients. + +This translation turns the `.vi` interface into a module type, the `.v` +implementation into a module, and uses opaque module ascription to hide them +module contents. +The only visible side effects are those that appear in the interface: here, +only `Global Open Scope Z_scope`. As we only `Require` stdpp.prelude in the +module body, we intend this to be **hidden** from clients that perform `Require +lib`, even if this might not be guaranteed by ``lib_composed.v`. ## Only a `.v` File From 3231fbf1d8831806a3359cf10af9643d3f8994ec Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 13 Feb 2022 01:05:01 +0100 Subject: [PATCH 19/30] s/value/answer/ to match the later example Also change the later example. --- text/separate-compilation.md | 28 +++++++++++++++------------- 1 file changed, 15 insertions(+), 13 deletions(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 1bc859ea..5d75a903 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -62,17 +62,17 @@ For concreteness, consider the following example: ```coq (* lib.vi *) Global Open Scope Z_scope. -Parameter value : nat. -Axiom value_is_42 : value = 42%nat. +Parameter answer : nat. +Axiom answer_is_42 : answer = 42%nat. (* lib.v *) Require Import stdpp.prelude. Global Open Scope N_scope. -Definition value : nat := 42. -Definition value_is_42 : value = 42%nat := ltac:(reflexivity). +Definition answer : nat := 42. +Definition answer_is_42 : answer = 42%nat := ltac:(reflexivity). -Definition other_value : N := 42. +Definition other_answer : N := 42 + 1. ``` Here, `lib.v` contains both the implementation of `lib.vi` and some commands @@ -87,16 +87,16 @@ following Coq source: (* lib_composed.v: *) Module Type __LIB. Global Open Scope Z_scope. - Parameter value : nat. - Axiom value_is_42 : value = 42. + Parameter answer : nat. + Axiom answer_is_42 : answer = 42. End __LIB. Module __lib : __LIB. Require Import stdpp.prelude. Global Open Scope N_scope. - Definition value : nat := 42. - Definition value_is_42 : value = 42%nat := ltac:(reflexivity). + Definition answer : nat := 42. + Definition answer_is_42 : answer = 42%nat := ltac:(reflexivity). End __lib. Export __lib. (* make the declarations from lib available from [Import]ing lib (rather that lib.lib *) @@ -141,6 +141,7 @@ Concretely, ```coq (* lib.vi *) +Global Open Scope Z_scope. Parameter answer : nat. Axiom answer_is_42 : answer = 42. ``` @@ -149,13 +150,14 @@ would be "translated" to: ```coq (* lib.v *) -Module Type LIB. +Module Type __LIB. + Global Open Scope Z_scope. Parameter answer : nat. Axiom answer_is_42 : answer = 42. -End LIB. +End __LIB. -Declare Module lib : LIB. -Export lib. +Declare Module __lib : __LIB. +Export __lib. ``` ## Universes From fc024801087668508c480eb452b8099c65522ab5 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 13 Feb 2022 01:06:56 +0100 Subject: [PATCH 20/30] Typo --- text/separate-compilation.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 5d75a903..3ca4e090 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -118,7 +118,7 @@ lib`, even if this might not be guaranteed by ``lib_composed.v`. It is crucial that having a `.v` file without a corresponding interface does *not* change the the current behavior of Coq. In Gallina, this is analagous to having a `Module` without a `Module Type` ascription. -In order to provide a uniform semantic understanding, we opt to reduce this to the previous situation in which both files exist, but note explictly that an implementation may not do this. For example, in Ocaml, a single `.ml` file does *not* generate a `.cmi` file. +In order to provide a uniform semantic understanding, we opt to reduce this to the previous situation in which both files exist, but note explicitly that an implementation may not do this. For example, in Ocaml, a single `.ml` file does *not* generate a `.cmi` file. The existance of dependent types and opaque definitions makes this question more subtle than the basic Ocaml solution. We see three solutions: From e1eb2c6fb09b0d293580c9697982c2a16d60845c Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 13 Feb 2022 01:08:03 +0100 Subject: [PATCH 21/30] Swap `.vi` only and `.v` only for better flow --- text/separate-compilation.md | 44 ++++++++++++++++++------------------ 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 3ca4e090..b076f32c 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -52,8 +52,8 @@ As a key principle: `.vi` interfaces are meant to hide implementations and suppo More concretely, our semantics for compiling top-level module (say, `lib`) distinguishes three scenarios, depending on the existence of: - both `lib.vi` and `lib.v`; -- only `lib.v`; -- or only `lib.vi`. +- only `lib.vi`; +- or only `lib.v`. ## Both a `.vi` and `.v` File @@ -113,26 +113,6 @@ only `Global Open Scope Z_scope`. As we only `Require` stdpp.prelude in the module body, we intend this to be **hidden** from clients that perform `Require lib`, even if this might not be guaranteed by ``lib_composed.v`. -## Only a `.v` File - -It is crucial that having a `.v` file without a corresponding interface does *not* change the the current behavior of Coq. -In Gallina, this is analagous to having a `Module` without a `Module Type` ascription. - -In order to provide a uniform semantic understanding, we opt to reduce this to the previous situation in which both files exist, but note explicitly that an implementation may not do this. For example, in Ocaml, a single `.ml` file does *not* generate a `.cmi` file. - -The existance of dependent types and opaque definitions makes this question more subtle than the basic Ocaml solution. -We see three solutions: - -1. *Verbatim* Synthesize the interface (the `.vi`) file using the *verbatim* contents of the `.v` file. This includes *all* definitions, hints, and other side effects. In particular it also includes the bodies of opaque (e.g. `Qed`d) defintions. While somewhat counter-intuitive, including the bodies of opaque definitions (as opposed to just their signature) means that we recover the exact semantics that we would get from including the implementation directly. -2. Synthesize the interface (the `.vi`) file using the contents of the `.v` file where opaque defintions (e.g. those that are `Qed`-d are replaced by `Parameter`s. There are two ways to do this: exactly and approximately. - - The *exact* characterization does not expose the body of the definition, but it does include its *full* characterization including universe constraints. Note that universe constraints may not be apparent from the type of the definition but they must still be included. - - The *approximate* characterization follows what a user would get from textually copying the type of the definition and converting it from a defined symbol to an assumed symbol, e.g. a `Parameter`. - - In this setup, the *exact* characterization is effectively the same as the first proposal, it simply changes the way that the opaque ascription is provided, i.e. from using `Qed` to using an opaque module ascription. - The *approximate* characterization follows (more closely) the semantics of `-vos` builds. This enables build parallelism at the cost of delayed universe checks (and all of the consequences of this). - -We note that both the *verbatim* proposal and the *exact* proposal are _effectively_ the same in the math. Aesthetically, we believe that the *exact* proposal seems cleaner, opting to hide more details from clients and use a more uniform sealing mechanism. The *Verbatim* option, on the other hand, seems more natural to understand and potentially implement. - ## Only a `.vi` File When only an interface file exists, there is (potentially) no underlying implementation, but the existance of the interface should still provide definite references to an implementation. @@ -160,6 +140,26 @@ Declare Module __lib : __LIB. Export __lib. ``` +## Only a `.v` File + +It is crucial that having a `.v` file without a corresponding interface does *not* change the the current behavior of Coq. +In Gallina, this is analagous to having a `Module` without a `Module Type` ascription. + +In order to provide a uniform semantic understanding, we opt to reduce this to the previous situation in which both files exist, but note explicitly that an implementation may not do this. For example, in Ocaml, a single `.ml` file does *not* generate a `.cmi` file. + +The existance of dependent types and opaque definitions makes this question more subtle than the basic Ocaml solution. +We see three solutions: + +1. *Verbatim* Synthesize the interface (the `.vi`) file using the *verbatim* contents of the `.v` file. This includes *all* definitions, hints, and other side effects. In particular it also includes the bodies of opaque (e.g. `Qed`d) defintions. While somewhat counter-intuitive, including the bodies of opaque definitions (as opposed to just their signature) means that we recover the exact semantics that we would get from including the implementation directly. +2. Synthesize the interface (the `.vi`) file using the contents of the `.v` file where opaque defintions (e.g. those that are `Qed`-d are replaced by `Parameter`s. There are two ways to do this: exactly and approximately. + - The *exact* characterization does not expose the body of the definition, but it does include its *full* characterization including universe constraints. Note that universe constraints may not be apparent from the type of the definition but they must still be included. + - The *approximate* characterization follows what a user would get from textually copying the type of the definition and converting it from a defined symbol to an assumed symbol, e.g. a `Parameter`. + + In this setup, the *exact* characterization is effectively the same as the first proposal, it simply changes the way that the opaque ascription is provided, i.e. from using `Qed` to using an opaque module ascription. + The *approximate* characterization follows (more closely) the semantics of `-vos` builds. This enables build parallelism at the cost of delayed universe checks (and all of the consequences of this). + +We note that both the *verbatim* proposal and the *exact* proposal are _effectively_ the same in the math. Aesthetically, we believe that the *exact* proposal seems cleaner, opting to hide more details from clients and use a more uniform sealing mechanism. The *Verbatim* option, on the other hand, seems more natural to understand and potentially implement. + ## Universes As some readers will anticipate, universe checks do not admit fully separate compilation; module bodies might add constraints absent from interfaces. This is already an issue with `.vos` builds today, and is a problem inherent to parallel builds, so any solutions to this problem could be shared. From 43e5f55e5280245265c2112f4ac7e7bf3345a549 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 13 Feb 2022 01:25:42 +0100 Subject: [PATCH 22/30] TODO: remove most of "only `v` file" --- text/separate-compilation.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index b076f32c..547fb09c 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -142,6 +142,15 @@ Export __lib. ## Only a `.v` File +If only a `.v` file is available, Coq's semantics should be the same as today: +the entire implementation shall be exposed in full builds, and it shall be +hidden in `vos` builds. + +TODO(Paolo): at this point, the rest of this section is unmotivated: it answers no +questions beyond the paragraph above. I am leaving it alone, but we need to +either explain why the different interfaces matter (which might be explained +later), or delete the rest of the section. + It is crucial that having a `.v` file without a corresponding interface does *not* change the the current behavior of Coq. In Gallina, this is analagous to having a `Module` without a `Module Type` ascription. @@ -180,6 +189,8 @@ A further issue is that universe inference does not seem to be prone to parallel ### "Link-time" Universe Checking +TODO(Paolo): to remove? The above seems an (incomplete) rewrite. + Cardelli's separate compilation has a further demand: in this example, if `consumer.v` typechecks, and `producer.v` satisfies its interface, the two shall link successfully. In Coq this is true except for universe constraints, like for existing `.vos` builds. To alleviate this problem, we propos`extending `.vok` outputs to i`lude proof terms, or at least universe constraint`so that we can r` a "link-time checker" that loads the whole program and checks whether combined universe constraints are satisfiable`The above assumes that u`verses and universe constraints for a term can be generated in isolation. However, universe inference is sometimes too greedy: when compiling `consumer.v` without the universe constraints from `producer.v`, Coq will sometimes produce different terms`for instance, some Ltac c` fail with an universe inconsistency and backtrack (as mentioned in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/vos.2Fvok.20and.20link-time.20universe.20check); we propose that the extra constraints be hidden at this stag`sometimes, Coq also seems t`produce stricter universe constraints than strictly needed, as Gaëtan shows in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Why.20does.20my.20fix.20for.20a.20universe.20problem.20work.3F/near/264903292. It'd be nice if the constraints were produced modularly, even if this might produce bigger graphs (hopefully in a tolerable way), or might require manual eta-expansion (we'd need Coq to give a warning/error when it must eta-expand, suggesting the user do that by hand)` ### "Full compilation" Semantics From e533ad28fbadf2cd569ab873cda565575d558842 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 13 Feb 2022 01:36:36 +0100 Subject: [PATCH 23/30] Typos --- text/separate-compilation.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 547fb09c..97d43583 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -152,7 +152,7 @@ either explain why the different interfaces matter (which might be explained later), or delete the rest of the section. It is crucial that having a `.v` file without a corresponding interface does *not* change the the current behavior of Coq. -In Gallina, this is analagous to having a `Module` without a `Module Type` ascription. +In Gallina, this is analogous to having a `Module` without a `Module Type` ascription. In order to provide a uniform semantic understanding, we opt to reduce this to the previous situation in which both files exist, but note explicitly that an implementation may not do this. For example, in Ocaml, a single `.ml` file does *not* generate a `.cmi` file. @@ -173,7 +173,7 @@ We note that both the *verbatim* proposal and the *exact* proposal are _effectiv As some readers will anticipate, universe checks do not admit fully separate compilation; module bodies might add constraints absent from interfaces. This is already an issue with `.vos` builds today, and is a problem inherent to parallel builds, so any solutions to this problem could be shared. -We consider vos builds a special case of this proposal, where interfaces are inferred as the strictest possible ones for the given implementation; `.vi` files enable hiding more implementation details. In both cases, the interface omits universe constraints that are derived from hidden bodies (for vos builds, just Qed bodies). While some universe checks are performed anyway, omitted constraints might make the universe graph unsatisfiable. +We consider `vos` builds a special case of this proposal, where interfaces are inferred as the strictest possible ones for the given implementation; `.vi` files enable hiding more implementation details. In both cases, the interface omits universe constraints that are derived from hidden bodies (for `vos` builds, just `Qed` bodies). While some universe checks are performed anyway, omitted constraints might make the universe graph unsatisfiable. To remedy this problem, we propose an additional "global" check. By analogy with separate compilation in other languages, we call this "link-time" universe checking. @@ -191,7 +191,7 @@ A further issue is that universe inference does not seem to be prone to parallel TODO(Paolo): to remove? The above seems an (incomplete) rewrite. -Cardelli's separate compilation has a further demand: in this example, if `consumer.v` typechecks, and `producer.v` satisfies its interface, the two shall link successfully. In Coq this is true except for universe constraints, like for existing `.vos` builds. To alleviate this problem, we propos`extending `.vok` outputs to i`lude proof terms, or at least universe constraint`so that we can r` a "link-time checker" that loads the whole program and checks whether combined universe constraints are satisfiable`The above assumes that u`verses and universe constraints for a term can be generated in isolation. However, universe inference is sometimes too greedy: when compiling `consumer.v` without the universe constraints from `producer.v`, Coq will sometimes produce different terms`for instance, some Ltac c` fail with an universe inconsistency and backtrack (as mentioned in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/vos.2Fvok.20and.20link-time.20universe.20check); we propose that the extra constraints be hidden at this stag`sometimes, Coq also seems t`produce stricter universe constraints than strictly needed, as Gaëtan shows in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Why.20does.20my.20fix.20for.20a.20universe.20problem.20work.3F/near/264903292. It'd be nice if the constraints were produced modularly, even if this might produce bigger graphs (hopefully in a tolerable way), or might require manual eta-expansion (we'd need Coq to give a warning/error when it must eta-expand, suggesting the user do that by hand)` +Cardelli's separate compilation has a further demand: in this example, if `consumer.v` typechecks, and `producer.v` satisfies its interface, the two shall link successfully. In Coq this is true except for universe constraints, like for existing `.vos` builds. To alleviate this problem, we propos`extending `.vok` outputs to i`lude proof terms, or at least universe constraint`so that we can r` a "link-time checker" that loads the whole program and checks whether combined universe constraints are satisfiable`The above assumes that universes and universe constraints for a term can be generated in isolation. However, universe inference is sometimes too greedy: when compiling `consumer.v` without the universe constraints from `producer.v`, Coq will sometimes produce different terms`for instance, some Ltac c` fail with an universe inconsistency and backtrack (as mentioned in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/vos.2Fvok.20and.20link-time.20universe.20check); we propose that the extra constraints be hidden at this stage. Sometimes, Coq also seems to produce stricter universe constraints than strictly needed, as Gaëtan shows in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Why.20does.20my.20fix.20for.20a.20universe.20problem.20work.3F/near/264903292. It'd be nice if the constraints were produced modularly, even if this might produce bigger graphs (hopefully in a tolerable way), or might require manual eta-expansion (we'd need Coq to give a warning/error when it must eta-expand, suggesting the user do that by hand). ### "Full compilation" Semantics From 6f9dc0172f24deabd97aa8dca55b5fce53fa384b Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Sun, 13 Feb 2022 12:07:24 +0000 Subject: [PATCH 24/30] Removals agreed with Gregory --- text/separate-compilation.md | 28 ---------------------------- 1 file changed, 28 deletions(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 97d43583..7a5d7bbd 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -146,29 +146,6 @@ If only a `.v` file is available, Coq's semantics should be the same as today: the entire implementation shall be exposed in full builds, and it shall be hidden in `vos` builds. -TODO(Paolo): at this point, the rest of this section is unmotivated: it answers no -questions beyond the paragraph above. I am leaving it alone, but we need to -either explain why the different interfaces matter (which might be explained -later), or delete the rest of the section. - -It is crucial that having a `.v` file without a corresponding interface does *not* change the the current behavior of Coq. -In Gallina, this is analogous to having a `Module` without a `Module Type` ascription. - -In order to provide a uniform semantic understanding, we opt to reduce this to the previous situation in which both files exist, but note explicitly that an implementation may not do this. For example, in Ocaml, a single `.ml` file does *not* generate a `.cmi` file. - -The existance of dependent types and opaque definitions makes this question more subtle than the basic Ocaml solution. -We see three solutions: - -1. *Verbatim* Synthesize the interface (the `.vi`) file using the *verbatim* contents of the `.v` file. This includes *all* definitions, hints, and other side effects. In particular it also includes the bodies of opaque (e.g. `Qed`d) defintions. While somewhat counter-intuitive, including the bodies of opaque definitions (as opposed to just their signature) means that we recover the exact semantics that we would get from including the implementation directly. -2. Synthesize the interface (the `.vi`) file using the contents of the `.v` file where opaque defintions (e.g. those that are `Qed`-d are replaced by `Parameter`s. There are two ways to do this: exactly and approximately. - - The *exact* characterization does not expose the body of the definition, but it does include its *full* characterization including universe constraints. Note that universe constraints may not be apparent from the type of the definition but they must still be included. - - The *approximate* characterization follows what a user would get from textually copying the type of the definition and converting it from a defined symbol to an assumed symbol, e.g. a `Parameter`. - - In this setup, the *exact* characterization is effectively the same as the first proposal, it simply changes the way that the opaque ascription is provided, i.e. from using `Qed` to using an opaque module ascription. - The *approximate* characterization follows (more closely) the semantics of `-vos` builds. This enables build parallelism at the cost of delayed universe checks (and all of the consequences of this). - -We note that both the *verbatim* proposal and the *exact* proposal are _effectively_ the same in the math. Aesthetically, we believe that the *exact* proposal seems cleaner, opting to hide more details from clients and use a more uniform sealing mechanism. The *Verbatim* option, on the other hand, seems more natural to understand and potentially implement. - ## Universes As some readers will anticipate, universe checks do not admit fully separate compilation; module bodies might add constraints absent from interfaces. This is already an issue with `.vos` builds today, and is a problem inherent to parallel builds, so any solutions to this problem could be shared. @@ -187,11 +164,6 @@ We have two problems: A further issue is that universe inference does not seem to be prone to parallelism. Without seeing `producer.v`, -### "Link-time" Universe Checking - -TODO(Paolo): to remove? The above seems an (incomplete) rewrite. - -Cardelli's separate compilation has a further demand: in this example, if `consumer.v` typechecks, and `producer.v` satisfies its interface, the two shall link successfully. In Coq this is true except for universe constraints, like for existing `.vos` builds. To alleviate this problem, we propos`extending `.vok` outputs to i`lude proof terms, or at least universe constraint`so that we can r` a "link-time checker" that loads the whole program and checks whether combined universe constraints are satisfiable`The above assumes that universes and universe constraints for a term can be generated in isolation. However, universe inference is sometimes too greedy: when compiling `consumer.v` without the universe constraints from `producer.v`, Coq will sometimes produce different terms`for instance, some Ltac c` fail with an universe inconsistency and backtrack (as mentioned in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/vos.2Fvok.20and.20link-time.20universe.20check); we propose that the extra constraints be hidden at this stage. Sometimes, Coq also seems to produce stricter universe constraints than strictly needed, as Gaëtan shows in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Why.20does.20my.20fix.20for.20a.20universe.20problem.20work.3F/near/264903292. It'd be nice if the constraints were produced modularly, even if this might produce bigger graphs (hopefully in a tolerable way), or might require manual eta-expansion (we'd need Coq to give a warning/error when it must eta-expand, suggesting the user do that by hand). ### "Full compilation" Semantics From 086dfcaf6b1f1c758442844b81c95a8f1cef0431 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Sun, 13 Feb 2022 14:02:43 +0000 Subject: [PATCH 25/30] markdown fix. --- text/separate-compilation.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 7a5d7bbd..6339b58e 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -111,7 +111,7 @@ module contents. The only visible side effects are those that appear in the interface: here, only `Global Open Scope Z_scope`. As we only `Require` stdpp.prelude in the module body, we intend this to be **hidden** from clients that perform `Require -lib`, even if this might not be guaranteed by ``lib_composed.v`. +lib`, even if this might not be guaranteed by `lib_composed.v`. ## Only a `.vi` File From 11e2c718e11df51a87b0a9abb52df955ef044a10 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Sun, 13 Feb 2022 13:05:07 -0500 Subject: [PATCH 26/30] Revisions and formatting. --- text/separate-compilation.md | 106 +++++++++++++++++++++++------------ 1 file changed, 70 insertions(+), 36 deletions(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 6339b58e..c530f380 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -9,7 +9,7 @@ as `Module` and `Module Type`. These can be quite heavyweight in many instances, and have some limitations when it comes to separately compiling files and building generic libraries. To address these problems, and support information hiding and Cardelli-style separate -compilation, in this CEP we introduce a notion of Coq interface files, which we +compilation, in this CEP we propose a notion of Coq interface files, which we will call a `.vi` file, and which are inspired by OCaml's `.mli` files. Intuitively, a Coq interface file called `module.vi` defines the public interface for `module.v`. The `module.vi` interface shall enable developing and @@ -19,14 +19,13 @@ If both `module.vi` and `module.v` are present, `module.vi` shall act as an opaque ascription for the top-level module defined by `module.v`; this opaque ascription ensures that clients that typecheck against `module.vi` shall still typecheck against the combination of `module.vi` and `module.v`, regardless of -the implementation details of `module.v`,[^intro-universes] including any -non-logical side effects such as hints (but excluding [universes](#universes)). -Instead, without interfaces, adding implementations is sufficient to break -clients, and changing implementations can break clients again, hindering modular -development. +the implementation details of `module.v`, including any non-logical side effects +such as hints (but excluding [universes](#universes)). Instead, without +interfaces, adding implementations is sufficient to break clients, and changing +implementations can break clients again, hindering modular development. This has a few advantages compared to Coq's state of the art: -- It enables separate development: after agreeing `module.vi`, `module.v` and +- It enables separate development: after agreeing on `module.vi`, `module.v` and its clients can be developed independently. To ensure this, unlike today's opaque ascription, `.vi` files can even hide side effects due to `Require`. - It reduces compile-time dependencies and improves compile times, even compared @@ -47,7 +46,12 @@ source-to-source transformation, to be taken as an informal and _approximate_ specification. However, this is an approximate specification, because the exact semantics cannot be expressed via source-to-source transformation. -As a key principle: `.vi` interfaces are meant to hide implementations and support separate compilation in Cardelli's sense. Hence, compiling a module `consumer.v` that consumes the interface of `producer.vi` shall not depend (directly or indirectly) on the existence of `producer.v` or its contents. As a consequence, no change to `producer.v` can affect whether `consumer.v` typechecks. +As a key principle: `.vi` interfaces are meant to hide implementations and +support separate compilation in Cardelli's sense. Hence, compiling a module +`consumer.v` that consumes the interface of `producer.vi` shall not depend +(directly or indirectly) on the existence of `producer.v` or its contents. As a +consequence, no change to `producer.v` can affect whether `consumer.v` +typechecks. More concretely, our semantics for compiling top-level module (say, `lib`) distinguishes three scenarios, depending on the existence of: @@ -93,6 +97,9 @@ End __LIB. Module __lib : __LIB. Require Import stdpp.prelude. + (* ^ Require inside a Module is strongly discouraged. What is relevant is + that side effects of the Module are not visible outside of this Module + *even* when the Module is Import-ed *) Global Open Scope N_scope. Definition answer : nat := 42. @@ -106,7 +113,7 @@ In this example translation, we use the `\_\_` prefix for generated identifiers used as a translation device; these identifiers should be hidden from clients. This translation turns the `.vi` interface into a module type, the `.v` -implementation into a module, and uses opaque module ascription to hide them +implementation into a module, and uses opaque module ascription to hide the module contents. The only visible side effects are those that appear in the interface: here, only `Global Open Scope Z_scope`. As we only `Require` stdpp.prelude in the @@ -115,9 +122,11 @@ lib`, even if this might not be guaranteed by `lib_composed.v`. ## Only a `.vi` File -When only an interface file exists, there is (potentially) no underlying implementation, but the existance of the interface should still provide definite references to an implementation. -Casting this in the feature set of the current Coq ecosystem, this essentially translates to a `Declare Module` [^full-functorization]. -Concretely, +When only an interface file exists, there is (potentially) no underlying +implementation, but the existance of the interface should still provide definite +references to an implementation. Casting this in the feature set of the current +Coq ecosystem, this essentially translates to a `Declare Module` +[^full-functorization]. Concretely, ```coq (* lib.vi *) @@ -148,37 +157,62 @@ hidden in `vos` builds. ## Universes -As some readers will anticipate, universe checks do not admit fully separate compilation; module bodies might add constraints absent from interfaces. This is already an issue with `.vos` builds today, and is a problem inherent to parallel builds, so any solutions to this problem could be shared. - -We consider `vos` builds a special case of this proposal, where interfaces are inferred as the strictest possible ones for the given implementation; `.vi` files enable hiding more implementation details. In both cases, the interface omits universe constraints that are derived from hidden bodies (for `vos` builds, just `Qed` bodies). While some universe checks are performed anyway, omitted constraints might make the universe graph unsatisfiable. - -To remedy this problem, we propose an additional "global" check. By analogy with separate compilation in other languages, we call this "link-time" universe checking. - -Consider files `a.vi`, `a.v` and `b.v`, where `b.v` depends on `a.v`. Assume that `a.v` satisfies the interface in `a.vi` but adds universe constraints, and that `b.v` typechecks against `a.vi`. Moreover, assume that the universe constraints of `a.v` and `b.v` are both satisfiable in isolation. - -We have two problems: - -1. Composing the universe constraints of `a.v` and `b.v` might produce an unsatisfiable constraint set, but this is not detected. This can also occur in "vos-style" builds. -2. We can elaborate `a.v` and `b.v` separately, but their combination might produce an unsatisfiable universe graph. - -A further issue is that universe inference does not seem to be prone to parallelism. Without seeing `producer.v`, - - +As some readers will anticipate, universe checks do not admit fully separate +compilation. Module bodies might add universe constraints that are note explicit +(or even visible) from its interface. This is already an issue with `.vos` +builds today, and is a problem inherent to Coq's global universe graph and +(generally) implicit treatment of universes in the surface syntax, so any +solution to this problem could be shared. + +We consider `vos` builds a special case of this proposal, where interfaces are +inferred as the strictest possible ones for the given implementation; `.vi` +files enable hiding more implementation details. In both cases, the interface +omits universe constraints that are derived from hidden bodies (for `vos` +builds, just `Qed` bodies). While some universe checks are performed anyway, +omitted constraints might make the universe graph unsatisfiable. + +To remedy this problem, we propose an additional "global" check. By analogy with +separate compilation in other languages, we call this "link-time" universe +checking. Such a link-time would be effectively the same as `Require`ing all of +the modules in a library preferring their *implemenation* (`.v` file) rather +than their interface (`.vi` file). If the combined set of constraints is +satisfiable, then there is no problem. + +If the combined set of constraints is *not* satisfiable, then the problem must +arise from an interface not exposing a constraint that an implementation +requires. Diffing the universe constraints between an interface and an +implementation would provide the right information necessary to diagnose and fix +the problem. ### "Full compilation" Semantics -The notion of full compilation semantics, i.e. a sound full-build semantics akin to a "vo-style" build can be achieved (at the cost of build parallelism) by introducing a dependency between the `.vio` file and the `.vo` file and elaboring the resulting `.vio` file with universe constraints introduced by the implementation. It is important that this does not include other side-effects from the `.vo` such as hints, tactics, or plugin requirements. +The notion of full compilation semantics, i.e. a sound full-build semantics akin +to a "vo-style" build can be achieved (at the cost of build parallelism) by +introducing a dependency between the `.vio` file and the `.vo` file and +elaboring the resulting `.vio` file with universe constraints introduced by the +implementation. It is important that this does not include other side-effects +from the `.vo` such as hints, tactics, or plugin requirements. -[//]: # It might be desirable to use interfaces even when compiling "vo-style" rather than "vos-style". At least, it would be easier to check universes in such a mode. This means that compiling `consumer.v` would load `producer.vo` despite the existence of `producer.vi`. We propose that in this mode, most side effects of `producer.vo` shall be ignored anyway, including its `Require`-bound side effects. -However, the extra universe constraints from `producer.vo` compared to `producer.vos` are important. - # Implementation The implementation would require (at least) the following: 1. Extending the build infrastructure to support `.vi` compilation. -2. Modifying the implementation of `Require` to search for `.vio` files in addition to `.vo` files. For backwards compatibility, we believe it would be important to search for both `.vio` and `.vo` files *simultaneously* rather than first searching for a `.vio` and then for a `.vo` because the later would mean that adding a `.vi` files could change the library that is used. -3. We believe that the bit-level representation of `.vio` could be the same as `.vo` files, though an alternative would be to leverage the representation of `.vos` files (which might be the same). - -[^full-functorization]: An alternative characterization of `Declare Module` is to implicitly functorize all dependent modules over the module type of the declared module. This understanding of `Declare Module` does enable some additional flexibility at "link-time" but is beyond the scope of this proposal. +2. Modifying the implementation of `Require` to search for `.vio` files in + addition to `.vo` files. For backwards compatibility, we believe it would be + important to search for both `.vio` and `.vo` files *simultaneously* rather + than first searching for a `.vio` and then for a `.vo` because the later + would mean that adding a `.vi` files could change the library that is used. +3. We believe that the bit-level representation of `.vio` could be the same as + `.vo` files, though an alternative would be to leverage the representation of + `.vos` files (which might be the same). + + +# Footnotes + +[^full-functorization]: An alternative characterization of `Declare Module` is + to implicitly functorize all dependent modules over the module type of the + declared module. This understanding of `Declare Module` does enable some + additional flexibility at "link-time" but is beyond the scope of this + proposal. From bd2e5eb4709b243c65b0a41e7d7332a9abc02573 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Sun, 13 Feb 2022 13:08:02 -0500 Subject: [PATCH 27/30] Additional clarification. --- text/separate-compilation.md | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index c530f380..7a94ecf5 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -200,10 +200,11 @@ The implementation would require (at least) the following: 1. Extending the build infrastructure to support `.vi` compilation. 2. Modifying the implementation of `Require` to search for `.vio` files in - addition to `.vo` files. For backwards compatibility, we believe it would be - important to search for both `.vio` and `.vo` files *simultaneously* rather - than first searching for a `.vio` and then for a `.vo` because the later - would mean that adding a `.vi` files could change the library that is used. + addition to `.vo` files. For backwards compatibility, we believe it is + necessary to search for both `.vio` and `.vo` files *simultaneously* rather + than first searching for a `.vio` everywhere and then for a `.vo` everywhere + because the later would mean that adding a `.vi` files could change the + library that is used. 3. We believe that the bit-level representation of `.vio` could be the same as `.vo` files, though an alternative would be to leverage the representation of `.vos` files (which might be the same). From 71391baa667dfae91bab465e5c3ce0b7ab16dc61 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Mon, 14 Feb 2022 16:30:22 +0100 Subject: [PATCH 28/30] Minor revision --- text/separate-compilation.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 7a94ecf5..679d22c7 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -189,9 +189,9 @@ the problem. The notion of full compilation semantics, i.e. a sound full-build semantics akin to a "vo-style" build can be achieved (at the cost of build parallelism) by introducing a dependency between the `.vio` file and the `.vo` file and -elaboring the resulting `.vio` file with universe constraints introduced by the -implementation. It is important that this does not include other side-effects -from the `.vo` such as hints, tactics, or plugin requirements. +elaborating the resulting `.vio` file with universe constraints introduced by the +implementation. It is important that nothing but universe constraints (say +hints, tactics or plugin requirements) leak from `.vo` files into `.vio` files. # Implementation From 37a04a48da9e08f24d62698bdccd8b37d52f2782 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Mon, 14 Feb 2022 16:30:33 +0100 Subject: [PATCH 29/30] Alternative implementation strategy --- text/separate-compilation.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 679d22c7..947b8866 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -193,6 +193,14 @@ elaborating the resulting `.vio` file with universe constraints introduced by th implementation. It is important that nothing but universe constraints (say hints, tactics or plugin requirements) leak from `.vo` files into `.vio` files. +Alternatively, the extra universe constraints could be fetched directly from +`.vo` files without altering the `.vio` files: again, nothing but universe +constraints should leak from implementations to clients. + +In this case, we could maybe ensure that `.vio` files coincide across separate +builds and "full" builds. +To this end, processing `Require library` when building `client.vio` file might +have to not load constraints from `library.vo`, even in a full build. # Implementation From bd11d597d11586526038f1346f2b5c26982f4f22 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Mon, 14 Feb 2022 16:31:27 +0100 Subject: [PATCH 30/30] Implementation plan: mention build support --- text/separate-compilation.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/text/separate-compilation.md b/text/separate-compilation.md index 947b8866..ba2bbf83 100644 --- a/text/separate-compilation.md +++ b/text/separate-compilation.md @@ -216,6 +216,8 @@ The implementation would require (at least) the following: 3. We believe that the bit-level representation of `.vio` could be the same as `.vo` files, though an alternative would be to leverage the representation of `.vos` files (which might be the same). +4. Build support for the new mode; ideally, some code could be shared with + support for `vos` builds. # Footnotes