add inductive formalization of datalog from @mtzguido

project-everest · Feb 26, 2024 · 2ba237a · 2ba237a
1 parent ebe6941
commit 2ba237a
Show file tree

Hide file tree

Showing 3 changed files with 667 additions and 1 deletion.
diff --git a/Makefile.common b/Makefile.common
@@ -41,13 +41,14 @@ DIST_DIRECTORY=$(ZETA_HOME)/steel/dist
 
 INCLUDE_PATHS+=$(OUTPUT_DIRECTORY) $(SRC_DIRS) $(KRML_HOME)/krmllib $(KRML_HOME)/krmllib/obj $(STEEL_HOME)/lib/steel
 
+LOAD_PLUGIN ?= --load_cmxs steel
 FSTAR_OPTIONS=--odir $(OUTPUT_DIRECTORY) \
 		 $(OTHERFLAGS) \
 		 --cache_dir $(CACHE_DIRECTORY) \
 	         $(addprefix --include , $(INCLUDE_PATHS)) \
 		 --cache_checked_modules \
 		 --cmi \
-                 --load_cmxs steel
+                 $(LOAD_PLUGIN)
 
 FSTAR=$(FSTAR_HOME)/bin/fstar.exe $(FSTAR_OPTIONS) $(ALREADY_CACHED)