darcsweb - verified/Makefile

ROCQ = rocq c -Q . ""

.PHONY: extract proofs clean all

all: extract

# -- Extraction targets --

extract: ../gen/HtmlPure.hs ../gen/PathPure.hs

../gen:
	mkdir -p ../gen

html_pure.vo ../gen/HtmlPure.hs: html_pure.v | ../gen
	$(ROCQ) html_pure.v
	@# Add GHC pragma and required imports for Haskell extraction
	sed -i '1i{-# OPTIONS_GHC -w #-}' ../gen/HtmlPure.hs
	sed -i '/^module.*where/a import qualified Data.Bits\nimport qualified Data.Char' ../gen/HtmlPure.hs

path_pure.vo ../gen/PathPure.hs: path_pure.v | ../gen
	$(ROCQ) path_pure.v
	@# Add GHC pragma and required imports for Haskell extraction
	sed -i '1i{-# OPTIONS_GHC -w #-}' ../gen/PathPure.hs
	sed -i '/^module.*where/a import qualified Data.Bits\nimport qualified Data.Char' ../gen/PathPure.hs

# -- Proof targets --

proofs: html_pure_proofs.vo path_pure_proofs.vo

html_pure_proofs.vo: html_pure_proofs.v html_pure.vo
	$(ROCQ) html_pure_proofs.v

path_pure_proofs.vo: path_pure_proofs.v path_pure.vo
	$(ROCQ) path_pure_proofs.v

# -- Clean --

clean:
	rm -f *.vo *.vok *.vos *.glob .*.aux
	rm -f ../gen/HtmlPure.hs ../gen/PathPure.hs