Skip to content

Commit

Permalink
Makefile: Make sure OPAMCLI is 2.0 in all subshells
Browse files Browse the repository at this point in the history
Furthermore, make sure variables defined by calling opam are
created using :=, so opam is not called each time they are expanded
  • Loading branch information
Alasdair committed Dec 15, 2023
1 parent 330e706 commit 775f258
Showing 1 changed file with 7 additions and 5 deletions.
12 changes: 7 additions & 5 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -128,14 +128,16 @@ export SAIL_DIR
EXPLICIT_COQ_SAIL=yes
else
# Use sail from opam package
SAIL_DIR:=$(shell opam config var sail:share)
SAIL_DIR:=$(shell OPAMCLI=$(OPAMCLI) opam config var sail:share)
SAIL:=sail
endif
SAIL_LIB_DIR:=$(SAIL_DIR)/lib
export SAIL_LIB_DIR
SAIL_SRC_DIR:=$(SAIL_DIR)/src

LEM_DIR?=$(shell opam config var lem:share)
ifndef LEM_DIR
LEM_DIR:=$(shell OPAMCLI=$(OPAMCLI) opam config var lem:share)
endif
export LEM_DIR

C_WARNINGS ?=
Expand Down Expand Up @@ -366,17 +368,17 @@ riscv_hol_build: generated_definitions/hol4/$(ARCH)/riscvTheory.uo
.PHONY: riscv_hol riscv_hol_build

ifdef BBV_DIR
EXPLICIT_COQ_BBV = yes
EXPLICIT_COQ_BBV := yes
else
EXPLICIT_COQ_BBV = $(shell if opam config var coq-bbv:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi)
EXPLICIT_COQ_BBV := $(shell if OPAMCLI=$(OPAMCLI) opam config var coq-bbv:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi)
ifeq ($(EXPLICIT_COQ_BBV),yes)
#Coq BBV library hopefully checked out in directory above us
BBV_DIR = ../bbv
endif
endif

ifndef EXPLICIT_COQ_SAIL
EXPLICIT_COQ_SAIL = $(shell if opam config var coq-sail:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi)
EXPLICIT_COQ_SAIL := $(shell if OPAMCLI=$(OPAMCLI) opam config var coq-sail:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi)
endif

COQ_LIBS = -R generated_definitions/coq Riscv -R generated_definitions/coq/$(ARCH) $(ARCH) -R handwritten_support Riscv_common
Expand Down

0 comments on commit 775f258

Please sign in to comment.