remove ora submodule; should install coq-vst-ora via opam instead

Author: mansky1

.gitmodules

@@ -10,6 +10,3 @@
 [submodule "fcf"]
 	path = fcf
 	url = https://github.com/adampetcher/fcf.git
-[submodule "ora"]
-	path = ora
-	url = https://github.com/mansky1/ora

Makefile

@@ -281,7 +281,7 @@ COMPCERTDIRS=lib common $(ARCHDIRS) cfrontend export $(BACKEND)
 
 ifeq ($(COMPCERT_EXPLICIT_PATH),true)
   COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT_INST_DIR)/$(d) compcert.$(d)) $(FLOCQ)
-  EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT_INST_DIR)/$(d) compcert.$(d)) $(FLOCQ) -Q ora/theories iris_ora
+  EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT_INST_DIR)/$(d) compcert.$(d)) $(FLOCQ)
 else
   COMPCERT_R_FLAGS=
   EXTFLAGS=
@@ -325,12 +325,6 @@ ifdef MATHCOMP
 EXTFLAGS:=$(EXTFLAGS) -R $(MATHCOMP) mathcomp
 endif
 
-# ##### ORA Flags #####
-
-ifneq ($(wildcard ora/theories),)
-EXTFLAGS:=$(EXTFLAGS) -Q ora/theories iris_ora
-endif
-
 # ##### refinedVST Flags #####
 EXTFLAGS:=$(EXTFLAGS) -Q refinedVST/lithium VST.lithium -Q refinedVST/typing VST.typing
 
@@ -404,17 +398,6 @@ MSL_FILES = \
   boolean_alg.v tree_shares.v shares.v pshares.v \
   Coqlib2.v sepalg_list.v
 
-ORA_FILES = \
-  theories/algebra/ora.v theories/algebra/excl.v theories/algebra/osum.v \
-  theories/algebra/agree.v theories/algebra/gmap.v theories/algebra/functions.v \
-  theories/algebra/dfrac.v theories/algebra/ext_order.v theories/algebra/view.v \
-  theories/algebra/auth.v theories/algebra/excl_auth.v theories/algebra/frac_auth.v \
-  theories/algebra/gmap_view.v theories/logic/oupred.v theories/logic/algebra.v \
-  theories/logic/iprop.v theories/logic/derived.v theories/logic/own.v \
-  theories/logic/proofmode.v theories/logic/logic.v theories/logic/wsat.v \
-  theories/logic/later_credits.v theories/logic/fancy_updates.v theories/logic/invariants.v \
-  theories/logic/cancelable_invariants.v theories/logic/weakestpre.v theories/logic/ghost_map.v
-
 SEPCOMP_FILES = \
   Address.v \
   effect_semantics.v \
@@ -673,7 +656,6 @@ C_FILES = $(SINGLE_C_FILES) $(LINKED_C_FILES)
 FILES = \
  veric/version.v \
  $(MSL_FILES:%=msl/%) \
- $(ORA_FILES:%=ora/%) \
  $(SEPCOMP_FILES:%=sepcomp/%) \
  $(VERIC_FILES:%=veric/%) \
  $(FLOYD_FILES:%=floyd/%) \
@@ -763,7 +745,7 @@ endif
 # ########## Targets ##########
 
 default_target: vst $(PROGSDIR)
-vst: _CoqProject msl veric ora floyd simpleconc
+vst: _CoqProject msl veric floyd simpleconc
 
 ifeq ($(BITSIZE),64)
 test: vst progs64
@@ -791,7 +773,6 @@ files: _CoqProject $(FILES:.v=.vo)
 #
 simpleconc: concurrency/conclib.vo atomics/verif_lock.vo
 msl:     _CoqProject $(MSL_FILES:%.v=msl/%.vo)
-ora:     _CoqProject $(ORA_FILES:%.v=ora/%.vo)
 sepcomp: _CoqProject $(CC_TARGET) $(SEPCOMP_FILES:%.v=sepcomp/%.vo)
 concurrency: _CoqProject $(CC_TARGET) $(SEPCOMP_FILES:%.v=sepcomp/%.vo) $(CONCUR_FILES:%.v=concurrency/%.vo)
 linking: _CoqProject $(LINKING_FILES:%.v=linking/%.vo)
@@ -841,7 +822,6 @@ install: VST.config
 	for d in $(sort $(dir $(INSTALL_FILES) $(EXTRA_INSTALL_FILES))); do install -d "$(INSTALLDIR)/$$d"; done
 	for f in $(INSTALL_FILES); do install -m 0644 $$f "$(INSTALLDIR)/$$(dirname $$f)"; done
 	for f in $(EXTRA_INSTALL_FILES); do install -m 0644 $$f "$(INSTALLDIR)/$$(dirname $$f)"; done
-	cd ora; $(MAKE) install
 
 dochtml:
 	mkdir -p doc/html
@@ -926,9 +906,6 @@ ifneq ($(wildcard InteractionTrees/theories),)
 #	$(COQDEP) -Q coq-ext-lib/theories ExtLib -Q paco/src Paco -Q InteractionTrees/theories ITree InteractionTrees/theories >>.depend
 	$(COQDEP) -Q paco/src Paco -Q InteractionTrees/theories ITree InteractionTrees/theories >>.depend
 endif
-ifneq ($(wildcard ora/theories),)
-	$(COQDEP) -Q ora/theories iris_ora ora/theories >>.depend
-endif
 ifneq ($(wildcard fcf/src/FCF),)
 	$(COQDEP) -Q fcf/src/FCF FCF fcf/src/FCF/*.v >>.depend
 endif
@@ -942,7 +919,6 @@ clean:
 	rm -f progs/VSUpile/{*,*/*}.{vo,vos,vok,glob}
 	rm -f progs64/VSUpile/{*,*/*}.{vo,vos,vok,glob}
 	rm -f progs/memmgr/*.{vo,vos,vok,glob}
-	rm -f ora/theories/*/*.{vo,vos,vok,glob}
 	rm -f coq-ext-lib/theories/*.{vo,vos,vok,glob} InteractionTrees/theories/{*,*/*}.{vo,vos,vok,glob}
 	rm -f paco/src/*.{vo,vos,vok,glob}
 	rm -f fcf/src/FCF/*.{vo,vos,vok,glob}

VERSION

@@ -1 +1 @@
-2.15
+3.1beta