Cleanup src Makefile

When we are building from git, we put the git version info in manifest.ml, so
we'll get the following from sail -v

Sail $last_git_tag ($branch @ $commit_sha)

If we are be built from opam we can't assume we are in a git repository as
opam downloads specific tags as tarballs, so instead we check for the precense
of SHARE_DIR which is set by our opam build script, and instead output

Sail 0.8 (sail2 @ opam)

which is the next git tag (current is 0.7.1, this must be updated by hand),
the branch name from which opam releases are generated and then opam rather
than the commit SHA.

I also removed the Makefile-non-opam file as it's bitrotted and unused

2 files changed, 10 insertions, 246 deletions

diff --git a/src/Makefile b/src/Makefile
index aeb23b9e..b0b22f77 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -62,16 +62,14 @@ endif
 endif
 
 
-.PHONY: all sail coverage sail.native sail.byte manifest.ml test clean doc lib power test_power test_idempotence
+.PHONY: all sail isail coverage sail.native sail.byte manifest.ml clean doc lib
 
 # set to -p on command line to enable gprof profiling
 OCAML_OPTS?=
 
-SHARE_DIR?=$(realpath ..)
-
 all: sail lib doc
 
-full: sail lib power doc test
+full: sail lib doc
 
 ast.lem: ../language/sail.ott
 	ott -sort false -generate_aux_rules true -o ast.lem -picky_multiple_parses true ../language/sail.ott
@@ -87,15 +85,19 @@ bytecode.ml: bytecode.lem
 	lem -ocaml bytecode.lem -lib . -lib gen_lib/
 	sed -i.bak -f ast.sed bytecode.ml
 
-lem_interp/interp_ast.lem: ../language/l2.ott
-	ott -sort false -generate_aux_rules true -o lem_interp/interp_ast.lem -picky_multiple_parses true ../language/l2.ott
-
 manifest.ml:
 	echo "(* Generated file -- do not edit. *)" > manifest.ml
-	echo let dir=\"$(SHARE_DIR)\" >> manifest.ml
+ifndef SHARE_DIR
+	echo let dir=\"$(realpath ..)\" >> manifest.ml
 	echo let commit=\"$(shell git rev-parse HEAD)\" >> manifest.ml
 	echo let branch=\"$(shell  git rev-parse --abbrev-ref HEAD)\" >> manifest.ml
 	echo let version=\"$(shell git describe)\" >> manifest.ml
+else
+	echo let dir=\"$(SHARE_DIR)\" >> manifest.ml
+	echo let commit=\"opam\" >> manifest.ml
+	echo let branch=\"sail2\" >> manifest.ml
+	echo let version=\"0.8\" >> manifest.ml
+endif
 
 sail: ast.ml bytecode.ml manifest.ml
 	ocamlbuild -use-ocamlfind sail.native sail_lib.cma sail_lib.cmxa
@@ -115,31 +117,10 @@ interpreter: lem_interp/interp_ast.lem
 	ocamlbuild -use-ocamlfind lem_interp/extract.cmxa
 	ocamlbuild -use-ocamlfind lem_interp/extract.cma
 
-test: sail interpreter
-	ocamlbuild -use-ocamlfind test/run_tests.native
-	./run_tests.native
-
 THIS_MAKEFILE := $(realpath $(lastword $(MAKEFILE_LIST)))
 SAIL_DIR:=$(realpath $(dir $(THIS_MAKEFILE))..)
 PROJECT_ROOT=$(realpath $(dir $(THIS_MAKEFILE))../..)
 
-_build/sail_values.ml: gen_lib/sail_values.ml
-	$(CP_TO_BUILD)
-
-_build/power.ml: $(SAIL_DIR)/src/test/power.sail sail.native
-	cd _build; \
-	./sail.native -lem_ast -ocaml $< -o $(basename $(@))
-
-_build/power.native: _build/sail_values.ml _build/power.ml
-	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package zarith -package unix -I _build -linkpkg $^ -o $@
-
-_build/armv8_embed.ml: sail.native
-	make -C ../arm ocaml
-	cp ../arm/build/armv8_embed.ml $@
-
-_build/arm.native: _build/sail_values.ml _build/armv8_embed.ml
-	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package zarith -package unix -I _build -linkpkg $^ -o $@
-
 clean:
 	-ocamlbuild -clean
 	-rm -rf _build *.native
diff --git a/src/Makefile-non-opam b/src/Makefile-non-opam
deleted file mode 100644
index ebd82c09..00000000
--- a/src/Makefile-non-opam
+++ /dev/null
@@ -1,217 +0,0 @@
-##########################################################################
-#     Sail                                                               #
-#                                                                        #
-#  Copyright (c) 2013-2017                                               #
-#    Kathyrn Gray                                                        #
-#    Shaked Flur                                                         #
-#    Stephen Kell                                                        #
-#    Gabriel Kerneis                                                     #
-#    Robert Norton-Wright                                                #
-#    Christopher Pulte                                                   #
-#    Peter Sewell                                                        #
-#    Alasdair Armstrong                                                  #
-#    Brian Campbell                                                      #
-#    Thomas Bauereiss                                                    #
-#    Anthony Fox                                                         #
-#    Jon French                                                          #
-#    Dominic Mulligan                                                    #
-#    Stephen Kell                                                        #
-#    Mark Wassell                                                        #
-#                                                                        #
-#  All rights reserved.                                                  #
-#                                                                        #
-#  This software was developed by the University of Cambridge Computer   #
-#  Laboratory as part of the Rigorous Engineering of Mainstream Systems  #
-#  (REMS) project, funded by EPSRC grant EP/K008528/1.                   #
-#                                                                        #
-#  Redistribution and use in source and binary forms, with or without    #
-#  modification, are permitted provided that the following conditions    #
-#  are met:                                                              #
-#  1. Redistributions of source code must retain the above copyright     #
-#     notice, this list of conditions and the following disclaimer.      #
-#  2. Redistributions in binary form must reproduce the above copyright  #
-#     notice, this list of conditions and the following disclaimer in    #
-#     the documentation and/or other materials provided with the         #
-#     distribution.                                                      #
-#                                                                        #
-#  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    #
-#  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     #
-#  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       #
-#  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   #
-#  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          #
-#  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      #
-#  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      #
-#  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   #
-#  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    #
-#  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    #
-#  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    #
-#  SUCH DAMAGE.                                                          #
-##########################################################################
-
-THIS_MAKEFILE := $(lastword $(MAKEFILE_LIST))
-# NOTE: it matters that this path is *not* canonicalised (realpath'd).
-# If we realpath it, the ocaml deps files will include realpaths, and
-# make won't know they're the same CMX files that we're building. So
-# will not correctly merge dependency subgraphs, and we will not build
-# stuff in the right order.
-# In general, the lesson is that the whole system needs to use the same
-# path, whether absolute or relative, to name a given file.
-# Sometimes that's difficult. Rules which cd to another directory break
-# if we're using absolute paths. I have used $(realpath $(srcdir)) in
-# those cases. This is not ideal. We shouldn't cd unless we really have to.
-srcdir := $(dir $(THIS_MAKEFILE))
-$(warning srcdir is $(srcdir))
-
-BITSTRING ?= $(srcdir)/contrib/bitstring
-BATTERIES ?= $(srcdir)/contrib/batteries-included/_build/src
-UINT ?= $(srcdir)/contrib/ocaml-uint/_build/lib
-
-export CAML_LD_LIBRARY_PATH := $(BITSTRING) $(CAML_LD_LIBRARY_PATH)
-
-LEM ?= ~/bitbucket/lem/lem
-LEMLIB ?= ~/bitbucket/lem/ocaml-lib/_build/
-OCAMLFLAGS +=  -I $(LEMLIB) # FIXME
-
-.PHONY: all sail test clean doc lib power test_power test_idempotence contrib install_elf
-all: sail lib doc
-full: all power test test
-sail: sail.native sail_lib.cma sail_lib.cmxa
-interpreter: _build/lem_interp/extract.cmxa _build/lem_interp/extract.cma
-sail.native sail_lib.cma sail_lib.cmxa:
-	ocamlbuild sail.native sail_lib.cma sail_lib.cmxa
-_build/lem_interp/extract.cmxa:
-	ocamlbuild lem_interp/extract.cmxa
-_build/lem_interp/extract.cma:
-	ocamlbuild lem_interp/extract.cma
-test: sail interpreter
-	ocamlbuild test/run_tests.native
-	./run_tests.native
-contrib:
-	cd contrib && ./checkout.sh
-install_elf:
-	cp -p ../../system-v-abi/src/*.lem elf_model/
-	cp -p ../../system-v-abi/src/*.ml elf_model/
-
-%.ml: %.lem
-	$(LEM) -outdir $$(dirname "$<") -ocaml -only_changed_output "$<"
-# HACK: special case for bitstring_local
-elf_model/bitstring_local.ml: elf_model/bitstring.lem
-	$(LEM) -outdir $$(dirname "$<") -ocaml -only_changed_output "$<"
-
-ELF_LEM_SRC := $(addprefix elf_model/,missing_pervasives.lem show.lem endianness.lem bitstring.lem elf_types.lem elf_interpreted_segment.lem elf_header.lem elf_file1.lem elf_program_header_table.lem elf_executable_file2.lem elf_section_header_table.lem elf_executable_file3.lem string_table.lem elf_executable_file4.lem elf_executable_file5.lem sail_interface.lem main.lem)
-vpath _build/%.lem .
-vpath _build/%.cmx .
-
-CAMLP4FLAGS += -nolib 
-CAMLP4FLAGS += -I $(srcdir)/contrib/$(BITSTRING)
-CAMLP4FLAGS += -parser o -parser op -printer p
-CAMLP4FLAGS += unix.cma 
-CAMLP4FLAGS += bitstring.cma 
-CAMLP4FLAGS += bitstring_persistent.cma 
-CAMLP4FLAGS += pa_bitstring.cmo
-
-# HACK: rewrite for bitstring_local
-ELF_ML_LEM := $(filter-out elf_model/bitstring.ml,$(patsubst %.lem,%.ml,$(ELF_LEM_SRC))) elf_model/bitstring_local.ml
-ELF_ML_SRC := $(addprefix elf_model/,error.ml ml_bindings.ml)  
-ELF_ML := $(ELF_ML_SRC) $(ELF_ML_LEM)
-ELF_ML_DEPS := $(patsubst %.ml,%.d,$(ELF_ML))
-ELF_CMX := $(patsubst %.ml,%.cmx,$(ELF_ML))
-
-$(ELF_CMX): OCAMLFLAGS += \
--I $(BITSTRING) -pp 'env CAML_LD_LIBRARY_PATH=$(BITSTRING) camlp4o $(CAMLP4FLAGS)' \
--I $(BATTERIES) \
--I $(UINT) \
--I $(srcdir)/elf_model
-
-$(ELF_ML_DEPS): OCAMLFLAGS += \
--I $(BITSTRING) -pp 'env CAML_LD_LIBRARY_PATH=$(BITSTRING) camlp4o $(CAMLP4FLAGS)' \
--I $(BATTERIES) \
--I $(UINT) \
--I $(srcdir)/elf_model
-
-$(ELF_ML_DEPS): %.d: %.ml
-	ocamldep -native $(OCAMLFLAGS) "$<" > "$@" || (rm -f "$@"; false)
-
-ifneq ($(MAKECMDGOALS),clean)
-include $(ELF_ML_DEPS)
-endif
-
-elf_extract.cmxa: OCAMLFLAGS += \
--I $(BITSTRING) -package bitstring,bitstring.syntax -syntax bitstring \
--I $(BATTERIES) -package batteries \
--I $(UINT) -package bitstring \
--pp 'camlp4 $(CAMLP4FLAGS)' \
--I $(LEMLIB)/../ocaml-lib/_build
-
-LEM_CMX :=  $(addprefix $(LEMLIB)/../ocaml-lib/,nat_num.cmx lem.cmx lem_function.cmx lem_list.cmx)
-
-%.cmx: %.ml
-	echo CAML_LD_LIBRARY_PATH is $$CAML_LD_LIBRARY_PATH 
-	ocamlopt $(OCAMLFLAGS) -c "$<"
-
-elf_model/elf_extract.cmxa: $(ELF_CMX)
-	ocamlopt $(OCAMLFLAGS) -a -o "$@" $+
-
-elf: $(ELF_CMX) $(LEM_CMX) elf_model/elf_extract.cmxa
-
-_build/test/power.lem: sail.native test/power.sail
-	mkdir -p _build/test
-	cp -p test/* _build/test/
-	cd _build/test && \
-	../../sail.native -lem_ast power.sail
-
-pprint/src/_build/PPrintLib.cmxa:
-	$(MAKE) -C $(srcdir)/pprint/src
-
-_build/test/run_power.native: OCAMLFLAGS += \
--I $(LEMLIB) \
--I $(srcdir)/_build/lem_interp/ \
--I $(srcdir)/elf_model/ \
--I $(UINT) 
-
-_build/test/run_power.native: OCAMLLIBS += \
-$(LEMLIB)/extract.cmxa
-
-_build/test/power.ml: _build/test/power.lem
-	cd _build/test && $(LEM) -ocaml -only_changed_output -lib $(realpath $(srcdir))/lem_interp/ power.lem
-	touch "$@" # HACK HACK HACK! why didn't lem update the timestamp?
-
-_build/test/run_power.native: pprint/src/_build/PPrintLib.cmxa _build/lem_interp/extract.cmxa elf_model/elf_extract.cmxa _build/test/power.ml test/run_power.ml
-	cd _build/test && \
-	ocamlopt $(OCAMLFLAGS) $(OCAMLLIBS) -I $(realpath $(srcdir))/_build/lem_interp $(addprefix $(realpath $(srcdir))/,$+) -o run_power.native
-
-power: run_power.native
-
-run_power.native: _build/test/run_power.native
-	ln -fs _build/test/run_power.native run_power.native
-
-test_power: power
-	./run_power.native --file ../../../rsem/idl/power/binary/main.bin
-
-test_power_interactive: power
-	./run_power.native --interactive --file ../../../rsem/idl/power/binary/main.bin
-
-test_power_interactive_srcs:
-	ebig ~/rsem/idl/power/generated/power.sail ../../../rsem/idl/power/binary/hello.c  ../../../rsem/idl/power/binary/hello.s 
-
-# or test/power.sail for cut-down one
-
-test_idempotence: sail
-	@cd test; for file in *.sail; do \
-		./idempotence.sh $$file; echo ;\
-	done
-
-clean:
-	#-ocamlbuild -clean
-	-rm -rf _build *.native
-	-rm -rf $(srcdir)/elf_model/*.o $(srcdir)/elf_model/*.cmx $(srcdir)/elf_model/*.cmi $(ELF_ML_LEM) $(ELF_ML_DEPS)
-	-rm -rf html-doc
-	-rm -rf tex-doc
-	-rm -rf lem lib
-	-rm -rf sail.docdir
-
-doc:
-	ocamlbuild sail.docdir/index.html
-
-lib:
-	ocamlbuild pretty_print.cmxa pretty_print.cma