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

Jump to bottom

Refactor examples makefile to simplify extraction tests. #15

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Refactor examples makefile to simplify extraction tests. #15

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
50 changes: 16 additions & 34 deletions share/pulse/examples/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ INCLUDE_PATHS += $(PULSE_HOME)/lib/pulse/c
OUTPUT_DIRECTORY=_output
CACHE_DIRECTORY=$(OUTPUT_DIRECTORY)/cache

.PHONY: all
all: verify test dice

include $(PULSE_SHARE)/Makefile.include
Expand All @@ -14,46 +15,27 @@ include $(PULSE_SHARE)/Makefile.include
dice:
+$(MAKE) -C dice

ifeq (,$(CACHE_DIRECTORY))
extractiontest_fst_checked=ExtractionTest.fst.checked
else
extractiontest_fst_checked=$(CACHE_DIRECTORY)/ExtractionTest.fst.checked
endif
EXTRA_KRML_OPTS=-skip-linking

extract: $(extractiontest_fst_checked)
# $(FSTAR) --odir $(OUTPUT_DIRECTORY) --codegen OCaml CustomSyntax.fst --extract CustomSyntax
$(FSTAR) --codegen OCaml ExtractionTest.fst --extract ExtractionTest
$(OUTPUT_DIRECTORY)/%.c: $(OUTPUT_DIRECTORY)/%.krml
$(KRML_HOME)/krml -bundle $*=* $(EXTRA_KRML_OPTS) $< -tmpdir $(OUTPUT_DIRECTORY)

extract_c: $(extractiontest_fst_checked)
$(FSTAR) --codegen krml ExtractionTest.fst --extract ExtractionTest
$(KRML_HOME)/krml -bundle ExtractionTest=* -skip-compilation $(OUTPUT_DIRECTORY)/ExtractionTest.krml -tmpdir $(OUTPUT_DIRECTORY)
.PHONY: extract
extract: $(OUTPUT_DIRECTORY)/ExtractionTest.ml

# $(FSTAR) --codegen krml Demo.MultiplyByRepeatedAddition.fst --extract '* -Pulse.Lib.Core'
# $(FSTAR_HOME)/../karamel/krml -bundle Demo.MultiplyByRepeatedAddition=* -skip-compilation $(OUTPUT_DIRECTORY)/out.krml
.PHONY: extract_c
extract_c: $(OUTPUT_DIRECTORY)/ExtractionTest.c

.PHONY: extract_pulse_c
extract_pulse_c: $(OUTPUT_DIRECTORY)/PulsePointStruct.c

ifneq (,$(KRML_HOME))
.PHONY: test-cbor
test-cbor: dice
+$(MAKE) -C dice/cbor

ifeq (,$(CACHE_DIRECTORY))
pulsepointstruct_fst_checked=c/PulsePointStruct.fst.checked
else
pulsepointstruct_fst_checked=$(CACHE_DIRECTORY)/PulsePointStruct.fst.checked
endif

extract_pulse_c: $(pulsepointstruct_fst_checked)
$(FSTAR) --odir $(OUTPUT_DIRECTORY) --codegen krml PulsePointStruct.fst --extract PulsePointStruct
$(KRML_HOME)/krml -bundle PulsePointStruct=* -skip-linking $(OUTPUT_DIRECTORY)/PulsePointStruct.krml -tmpdir $(OUTPUT_DIRECTORY)

.PHONY: test
ifeq (,$(KRML_HOME))
test: extract
else
test-cbor:

extract_pulse_c:

test: extract test-cbor extract_c extract_pulse_c
endif

test: test-cbor extract_pulse_c

.PHONY: extract_pulse_c

.PHONY: test test-cbor test-cbor-raw
Loading