Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Qualify imports to disable race condition for opam builds #1001

Merged
merged 3 commits into from
Nov 1, 2023
Merged

Qualify imports to disable race condition for opam builds #1001

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
018a348
eliminate race condition for opam compilation
yforster Nov 1, 2023
6455ca3
disable quick target in CI - it is not quicker
yforster Nov 1, 2023
309f107
fix Makefile and opam files
yforster Nov 1, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/build.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ jobs:
- '8.17'
ocaml_version:
- '4.14-flambda'
target: [ local, opam, quick ]
target: [ local, opam ]
fail-fast: true

concurrency:
Expand Down
2 changes: 1 addition & 1 deletion Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@

all: printconf template-coq pcuic safechecker erasure erasure-plugin
all: printconf template-coq pcuic safechecker erasure erasure-plugin safechecker-plugin quotation

-include Makefile.conf

Expand Down
2 changes: 1 addition & 1 deletion coq-metacoq-common.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ authors: ["Abhishek Anand <[email protected]>"
license: "MIT"
build: [
["bash" "./configure.sh"]
[make "-j" "%{jobs}%" "common"]
[make "-j" "%{jobs}%" "-C" "common"]
]
install: [
[make "-C" "common" "install"]
Expand Down
2 changes: 1 addition & 1 deletion coq-metacoq-template.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ authors: ["Abhishek Anand <[email protected]>"
license: "MIT"
build: [
["bash" "./configure.sh"]
[make "-j" "%{jobs}%" "template-coq"]
[make "-j" "%{jobs}%" "-C" "template-coq"]
]
install: [
[make "-C" "template-coq" "install"]
Expand Down
5 changes: 3 additions & 2 deletions erasure/theories/EWcbvEvalNamed.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
(* Distributed under the terms of the MIT license. *)
From Coq Require Import Utf8 Program.
From MetaCoq Require Import config utils BasicAst.
From MetaCoq.Utils Require Import utils.
From MetaCoq.Common Require Import config BasicAst.
From MetaCoq.PCUIC Require PCUICWcbvEval.
From MetaCoq.Erasure Require Import EAst EAstUtils ELiftSubst ECSubst EReflect EGlobalEnv
EWellformed EWcbvEval.
Expand Down Expand Up @@ -671,7 +672,7 @@ Local Notation "'⊩' v ~ s" := (represents_value v s) (at level 50).
Local Hint Constructors represents : core.
Local Hint Constructors represents_value : core.

From MetaCoq Require Import bytestring MCString.
From MetaCoq.Utils Require Import bytestring MCString.
Require Import BinaryString.
Import String.

Expand Down
Loading