Makefile

COQ_PATH =	_build/lib/coq/user-contrib
RUST_TARGET = $(shell rustc -vV | sed -n 's|host: ||p')
RUST_PATH =	target/$(RUST_TARGET)/release

CASE_STUDIES = case_studies/paper_examples case_studies/tests case_studies/minivec case_studies/evenint

### Project setup
setup-nix:
	rm -f dune-project
.PHONY: setup-nix

setup-dune:
	echo "(lang dune 3.8)" > dune-project
.PHONY: setup-dune

### generic build targets
generate_all: generate_stdlib generate_case_studies
.PHONY: generate_all

clean: clean_case_studies clean_stdlib
	@dune clean
.PHONY: clean

all_with_examples: all case_studies.proof
	dune build --display short
.PHONY: all_with_examples

### core components
typesystem:
	cd theories && dune build --display short
.PHONY: typesystem

frontend:
	cd rr_frontend && ./refinedrust build
.PHONY: frontend

all: frontend typesystem stdlib.proof
.PHONY: all

### case studies
case_studies.proof: typesystem generate_case_studies
	cd case_studies && dune build --display short
.PHONY: case_studies.proof

clean_case_studies: $(CASE_STUDIES:=.clean)
.PHONY: clean_case_studies

generate_case_studies:
generate_case_studies: $(CASE_STUDIES:=.crate)
.PHONY: generate_case_studies

case_studies/%.proof:	stdlib.proof case_studies/%.crate
	cd case_studies/$* && dune build --display short

### stdlib
stdlib.proof: typesystem generate_stdlib
	RUST_PATH=$(RUST_PATH) $(MAKE) -C stdlib stdlib.proof
.PHONY: stdlib.proof

clean_stdlib:
	RUST_PATH=$(RUST_PATH) $(MAKE) -C stdlib clean_stdlib
.PHONY: clean_stdlib

generate_stdlib:
	RUST_PATH=$(RUST_PATH) $(MAKE) -C stdlib generate_stdlib
.PHONY: generate_stdlib

### Calling the frontend
# this adds the path to the built frontend so cargo can find it
%.crate:	export PATH := $(CURDIR)/rr_frontend/$(RUST_PATH):$(PATH)
%.crate: %
	cd $* && cargo refinedrust

%.clean: phony
	cd $* && cargo clean
.PHONY: phony

### Builddep handling
# see https://stackoverflow.com/a/649462 for defining multiline strings in Makefiles
define BUILDDEP_OPAM_BODY
opam-version: "2.0"
name: "refinedrust-builddep"
maintainer: "RefinedRust contributors"
author: "RefinedRust contributors"
homepage: "https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev"
bug-reports: "https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev"
synopsis: "---"
description: """
---
"""
license: "BSD-3-Clause"
depends: [
endef
export BUILDDEP_OPAM_BODY

# Create a virtual Opam package with the same deps as RefinedC, but no
# build.
builddep/refinedrust-builddep.opam: theories/refinedrust.opam Makefile
	@echo "# Creating builddep package."
	@mkdir -p builddep
	@echo "$$BUILDDEP_OPAM_BODY" > $@
	@opam show -f depends: ./theories/refinedrust.opam >> $@
	@echo "]" >> $@

# Install the virtual Opam package to ensure that:
#  1) dependencies of RefinedRust are installed,
#  2) they will remain satisfied even if other packages are updated/installed,
#  3) we do not have to pin the RefinedRust package itself (which takes time).
builddep: builddep/refinedrust-builddep.opam
	@echo "# Installing package $^."
	@opam install $(OPAMFLAGS) $^
.PHONY: builddep


### Generating _CoqProject
define COQPROJECT_BASE_BODY
# RefinedRust core
-Q _build/default/theories/lithium lithium
-Q _build/default/theories/caesium caesium
-Q _build/default/theories/rust_typing refinedrust

-Q _build/default/case_studies/extra_proofs refinedrust.extra_proofs
endef
export COQPROJECT_BASE_BODY

coqproject-base:
	@echo "$$COQPROJECT_BASE_BODY" > _CoqProject

case_studies/%.coqproject: coqproject-base
	@echo "-Q _build/default/case_studies/$*/output/$* refinedrust.examples.$*" >> _CoqProject

coqproject-case-studies: $(CASE_STUDIES:=.coqproject)

coqproject: coqproject-base coqproject-case-studies