#################################################################-*-makefile-*-
# OPENTHEORY DEVELOPMENT MAKEFILE
# Copyright (c) 2005 Joe Leslie-Hurd, distributed under the MIT license
###############################################################################

.PRECIOUS: bin/mlton/%.sml bin/mlton/%.mlb bin/polyml/%.sml

###############################################################################
# Uncomment your default compiler.
###############################################################################

OPENTHEORY = bin/mlton/opentheory
#OPENTHEORY = bin/polyml/opentheory
#OPENTHEORY = bin/mosml/opentheory

###############################################################################
# Cleaning temporary files.
###############################################################################

TEMP += \
  bin/mlton/*.ssa bin/mlton/*.ssa2 bin/mlton/basis.sml \
  bin/mlton/benchmark \
  mlmon.out profile-* benchmark.out

###############################################################################
# The ML preprocessor.
###############################################################################

MLPP_OPTS += -r 'OpenTheoryDebug'
#MLPP_OPTS += -r 'BasicDebug|OpenTheoryDebug'
#MLPP_OPTS += -r 'BasicDebug|OpenTheoryDebug|OpenTheoryTrace[0-9]'

###############################################################################
# The Moscow ML compiler.
###############################################################################

MOSML_DEP = scripts/mosml_dep

bin/mosml/Makefile.src: Makefile Makefile.dev $(MOSML_DEP) $(MLPP)
	@echo
	@echo '+--------------------------------------------------+'
	@echo '| Regenerating the Moscow ML makefile dependencies |'
	@echo '+--------------------------------------------------+'
	@echo
	@$(MOSML_DEP) $(MOSML_SRC) $(MOSML_TARGETS) > $@

###############################################################################
# The MLton compiler.
###############################################################################

MLTON_OPTS += -verbose 1
#MLTON_OPTS += -const 'Exn.keepHistory true'
#MLTON_OPTS += -keep ssa -keep ssa2
#MLTON_OPTS += -show-basis basis.sml
#MLTON_OPTS += -inline 100000
#MLTON_OPTS += -const 'MLton.safe false' -const 'MLton.detectOverflow false'

###############################################################################
# Moving source files around.
###############################################################################

COPY = cp -v

src/selftest.sml: test/test.sml ; @$(COPY) $< $@

src/benchmark.sml: src/opentheory.sml ; @$(COPY) $< $@

###############################################################################
# Importing the basic library.
###############################################################################

BASIC_LIBRARY = ../basic

.PHONY: import-basic
import-basic:
	@$(COPY) $(BASIC_LIBRARY)/scripts/ml_lines $(LINES)
	@$(COPY) $(BASIC_LIBRARY)/scripts/mlpp $(MLPP)
	@$(COPY) $(BASIC_LIBRARY)/scripts/mosml_dep $(MOSML_DEP)
	@$(COPY) $(BASIC_LIBRARY)/scripts/release_stamp $(RELEASE_STAMP)
	@$(COPY) $(BASIC_LIBRARY)/src/Config.sig src/Config.sig
	@$(COPY) $(BASIC_LIBRARY)/src/Config.sml src/Config.sml
	@$(COPY) $(BASIC_LIBRARY)/src/ElementSet.sig src/ElementSet.sig
	@$(COPY) $(BASIC_LIBRARY)/src/ElementSet.sml src/ElementSet.sml
	@$(COPY) $(BASIC_LIBRARY)/src/Heap.sig src/Heap.sig
	@$(COPY) $(BASIC_LIBRARY)/src/Heap.sml src/Heap.sml
	@$(COPY) $(BASIC_LIBRARY)/src/Html.sig src/Html.sig
	@$(COPY) $(BASIC_LIBRARY)/src/Html.sml src/Html.sml
	@$(COPY) $(BASIC_LIBRARY)/src/KeyMap.sig src/KeyMap.sig
	@$(COPY) $(BASIC_LIBRARY)/src/KeyMap.sml src/KeyMap.sml
	@$(COPY) $(BASIC_LIBRARY)/src/Lazy.sig src/Lazy.sig
	@$(COPY) $(BASIC_LIBRARY)/src/Lazy.sml src/Lazy.sml
	@$(COPY) $(BASIC_LIBRARY)/src/Map.sig src/Map.sig
	@$(COPY) $(BASIC_LIBRARY)/src/Map.sml src/Map.sml
	@$(COPY) $(BASIC_LIBRARY)/src/Options.sig src/Options.sig
	@$(COPY) $(BASIC_LIBRARY)/src/Options.sml src/Options.sml
	@$(COPY) $(BASIC_LIBRARY)/src/Ordered.sig src/Ordered.sig
	@$(COPY) $(BASIC_LIBRARY)/src/Ordered.sml src/Ordered.sml
	@$(COPY) $(BASIC_LIBRARY)/src/Parse.sig src/Parse.sig
	@$(COPY) $(BASIC_LIBRARY)/src/Parse.sml src/Parse.sml
	@$(COPY) $(BASIC_LIBRARY)/src/Portable.sig src/Portable.sig
	@$(COPY) $(BASIC_LIBRARY)/src/PortableMosml.sml src/PortableMosml.sml
	@$(COPY) $(BASIC_LIBRARY)/src/PortableMlton.sml src/PortableMlton.sml
	@$(COPY) $(BASIC_LIBRARY)/src/PortablePolyml.sml src/PortablePolyml.sml
	@$(COPY) $(BASIC_LIBRARY)/src/Print.sig src/Print.sig
	@$(COPY) $(BASIC_LIBRARY)/src/Print.sml src/Print.sml
	@$(COPY) $(BASIC_LIBRARY)/src/Queue.sig src/Queue.sig
	@$(COPY) $(BASIC_LIBRARY)/src/Queue.sml src/Queue.sml
	@$(COPY) $(BASIC_LIBRARY)/src/Random.sig src/Random.sig
	@$(COPY) $(BASIC_LIBRARY)/src/Random.sml src/Random.sml
	@$(COPY) $(BASIC_LIBRARY)/src/Set.sig src/Set.sig
	@$(COPY) $(BASIC_LIBRARY)/src/Set.sml src/Set.sml
	@$(COPY) $(BASIC_LIBRARY)/src/Stream.sig src/Stream.sig
	@$(COPY) $(BASIC_LIBRARY)/src/Stream.sml src/Stream.sml
	@$(COPY) $(BASIC_LIBRARY)/src/Useful.sig src/Useful.sig
	@$(COPY) $(BASIC_LIBRARY)/src/Useful.sml src/Useful.sml
	@$(COPY) $(BASIC_LIBRARY)/src/VertexGraph.sig src/VertexGraph.sig
	@$(COPY) $(BASIC_LIBRARY)/src/VertexGraph.sml src/VertexGraph.sml

###############################################################################
# Export the Haskell theories.
###############################################################################

HASKELL_DIR = data/haskell

HASKELL_INSTALL = ../../../scripts/install-haskell

HASKELL_OPENTHEORY_EXPORT = ../../$(OPENTHEORY) export --haskell $(HASKELL_OPENTHEORY_EXPORT_OPTS)

HASKELL_OPENTHEORY_LIST = ../../$(OPENTHEORY) list --dependency-order ExportHaskell

HASKELL_EXTRA_PACKAGES = \
  api-opentheory-unicode \
  decode-utf8 \
  nth-prime \
  fen2s

.PHONY: clean-haskell
clean-haskell: $(OPENTHEORY)
	scripts/reset-haskell $(HASKELL_EXTRA_PACKAGES)

.PHONY: export-haskell
export-haskell: $(OPENTHEORY)
	@cd $(HASKELL_DIR) && ($(HASKELL_OPENTHEORY_LIST) | perl -ne 'my $$nv = $$_; chomp $$nv; print STDOUT "----------------------\n"; my $$cmd = "$(HASKELL_OPENTHEORY_EXPORT) $$nv"; print STDOUT "$$cmd\n"; my $$n = `$$cmd`; print STDOUT "$$n"; chomp $$n; if ($$n =~ /^(?:re-)?exported package [[:alnum:]-]+-[[:digit:].]+ as Haskell package ([[:alnum:]-]+)-[[:digit:].]+$$/m) { $$n = $$1; } elsif ($$n =~ /^skipped re-export of package [[:alnum:]-]+-[[:digit:].]+ as Haskell package ([[:alnum:]-]+)$$/m) { $$n = $$1; } else { die "bad export output |$$n|"; } (system("cd $$n && $(HASKELL_INSTALL)") == 0) or die;')

.PHONY: reexport-haskell
reexport-haskell:
	@HASKELL_OPENTHEORY_EXPORT_OPTS="--reexport" $(MAKE) export-haskell

.PHONY: haskell
haskell:
	@cd $(HASKELL_DIR)/opentheory-primitive && $(HASKELL_INSTALL)
	$(MAKE) export-haskell
	@echo ======================
	@cd $(HASKELL_DIR) && for f in $(HASKELL_EXTRA_PACKAGES) ; do cd $$f && $(HASKELL_INSTALL) && cd .. && echo ---------------------- ; done

###############################################################################
# Create the test package repo.
###############################################################################

TEST_THEORY_DIR = test/theories

TEST_REPOSITORY_DIR = test/repos/test

TEST_OPENTHEORY = $(OPENTHEORY) -d $(TEST_REPOSITORY_DIR)

TEST_OPENTHEORY_INIT = $(TEST_OPENTHEORY) init

TEST_OPENTHEORY_INSTALL = $(TEST_OPENTHEORY) install --manual

.PHONY: test-repository
test-repository:
	$(MAKE) $(OPENTHEORY)
	rm -rf $(TEST_REPOSITORY_DIR)
	$(TEST_OPENTHEORY_INIT)
	$(TEST_OPENTHEORY_INSTALL) $(TEST_THEORY_DIR)/empty/empty.thy
	$(TEST_OPENTHEORY_INSTALL) $(TEST_THEORY_DIR)/bool-true-def/bool-true-def.thy
	$(TEST_OPENTHEORY_INSTALL) $(TEST_THEORY_DIR)/bool-true-thm/bool-true-thm.thy
	$(TEST_OPENTHEORY_INSTALL) $(TEST_THEORY_DIR)/bool-true/bool-true.thy
	$(TEST_OPENTHEORY_INSTALL) $(TEST_THEORY_DIR)/bool-true-assert/bool-true-assert.thy
	$(TEST_OPENTHEORY_INSTALL) $(TEST_THEORY_DIR)/bool-true-axiom/bool-true-axiom.thy

###############################################################################
# Initialization following a repo clone.
###############################################################################

.PHONY: init
init:
	@echo
	@echo '+---------------------------------------------------+'
	@echo '| Initialize this development version of opentheory |'
	@echo '+---------------------------------------------------+'
	@echo
	@$(COPY) LICENSE doc/MIT-LICENSE
	$(MAKE) test-repository

###############################################################################
# Import and install HOL Light theories.
###############################################################################

HOL_LIGHT_DIR = ../hol-light

TEST_ARTICLE_DIR = test/articles

THEORY_DIR = data/theories

OPENTHEORY_INIT = $(OPENTHEORY) init

IMPORT_THEORIES = scripts/import-theories -p "HOL Light theory" -u

INSTALL_THEORIES = scripts/install-theories -u

CHECK_THEORIES = scripts/check-theories

UNAVAILABLE_THEORIES = '(Identity - OnRepo) All'

.PHONY: reset-directory
reset-directory: $(OPENTHEORY)
	rm -rf $(HOME)/.opentheory
	$(OPENTHEORY_INIT)

.PHONY: clean-theories
clean-theories: $(OPENTHEORY)
	$(OPENTHEORY) update
	@if $(OPENTHEORY) list --quiet $(UNAVAILABLE_THEORIES) ; then echo 'uninstalling theories that are not available from the repos:' ; $(OPENTHEORY) uninstall $(UNAVAILABLE_THEORIES) ; else echo 'all installed theories are available from the repos' ; fi
	@scripts/reinstall-theories

.PHONY: capture-theories
capture-theories: $(OPENTHEORY)
	$(MAKE) -C $(HOL_LIGHT_DIR)/opentheory theories

.PHONY: import-theories
import-theories: $(OPENTHEORY)
	@echo
	@echo '+--------------------------------+'
	@echo '| Import theories from HOL Light |'
	@echo '+--------------------------------+'
	@echo
	$(IMPORT_THEORIES) $(HOL_LIGHT_DIR)/opentheory/export

.PHONY: install-theories
install-theories: $(OPENTHEORY)
	@echo
	@echo '+--------------------------+'
	@echo '| Install updated theories |'
	@echo '+--------------------------+'
	@echo
	$(INSTALL_THEORIES)

.PHONY: check-theories
check-theories: $(OPENTHEORY)
	@echo
	@echo '+--------------------------+'
	@echo '| Check installed theories |'
	@echo '+--------------------------+'
	@echo
	$(CHECK_THEORIES)

.PHONY: theories
theories:
	$(MAKE) capture-theories
	$(MAKE) import-theories
	$(MAKE) install-theories
	$(MAKE) check-theories

.PHONY: tiny-theories
tiny-theories:
	$(MAKE) -C $(HOL_LIGHT_DIR)/opentheory tiny-theories
	cp $(HOL_LIGHT_DIR)/opentheory/export/*.art $(TEST_ARTICLE_DIR)/hol-light
	$(MAKE) clean
	$(MAKE) mlton
	cp $(TEST_ARTICLE_DIR)/bool-true-def.art $(TEST_THEORY_DIR)/bool-true-def/bool-true-def.art
	cp $(TEST_ARTICLE_DIR)/bool-true-thm.art $(TEST_THEORY_DIR)/bool-true-thm/bool-true-thm.art
	cp $(TEST_ARTICLE_DIR)/bool-forall-def.art $(TEST_THEORY_DIR)/bool-forall-def/bool-forall-def.art
	cp $(TEST_ARTICLE_DIR)/bool-forall-thm.art $(TEST_THEORY_DIR)/bool-forall-thm/bool-forall-thm.art
	cp $(TEST_ARTICLE_DIR)/bool-and-def.art $(TEST_THEORY_DIR)/bool-and-def/bool-and-def.art
	cp $(TEST_ARTICLE_DIR)/bool-and-thm.art $(TEST_THEORY_DIR)/bool-and-thm/bool-and-thm.art
	cp $(TEST_ARTICLE_DIR)/bool-and-thm-new.art $(TEST_THEORY_DIR)/bool-and-thm-1.1/bool-and-thm.art
	cp $(TEST_ARTICLE_DIR)/bool-implies-def.art $(TEST_THEORY_DIR)/bool-implies-def/bool-implies-def.art
	cp $(TEST_ARTICLE_DIR)/bool-implies-thm.art $(TEST_THEORY_DIR)/bool-implies-thm/bool-implies-thm.art
	cp $(TEST_ARTICLE_DIR)/bool-implies-thm-new.art $(TEST_THEORY_DIR)/bool-implies-thm-1.1/bool-implies-thm.art
	$(MAKE) init

###############################################################################
# Counting the number of lines of code.
###############################################################################

LINES = scripts/ml_lines

.PHONY: lines
lines: $(LINES)
	@echo
	@echo -n 'opentheory '
	@$(LINES) $(SRC) src/opentheory.sml
	@echo

###############################################################################
# Profiling using MLton.
###############################################################################

#BENCHMARK_OPTS = info --preserve-theory --article -o benchmark.out ../hol-light/opentheory/articles/char-utf8-thm.thy
BENCHMARK_OPTS = install ~/tmp/theory/hol-base/hol-base.thy

profile-time.mlb: bin/mlton/benchmark.sml
	echo '$$(SML_LIB)/basis/basis.mlb $$(SML_LIB)/basis/mlton.mlb $<' > $@

profile-time: profile-time.mlb
	@echo
	@echo '+------------------------------------------------------+'
	@echo '| Compile the OpenTheory benchmark with time profiling |'
	@echo '+------------------------------------------------------+'
	@echo
	$(MLTON) $(MLTON_OPTS) -profile time -profile-stack true -profile-branch true $<
	@echo

profile-time.out profile-time-log: profile-time
	time ./profile-time $(BENCHMARK_OPTS) | tee profile-time.log
	mv mlmon.out profile-time.out

profile-time.txt: profile-time.out Makefile.dev
	mlprof -show-line true -raw true -keep '(and (thresh 0.1) (thresh-stack 0.1))' -split '.*' profile-time profile-time.out > $@

profile-time.dot: profile-time.out Makefile.dev
	mlprof -show-line true -raw true -call-graph $@ -keep '(thresh-stack 5)' -graph-title "OpenTheory Time Profiling" -split '.*' profile-time profile-time.out > /dev/null

.PHONY: profile
profile: profile-time.txt profile-time.dot

###############################################################################
# Releasing.
###############################################################################

RELEASE_DIR = release

RELEASE_STAMP = scripts/release_stamp

.PHONY: release-stamp
release-stamp: $(RELEASE_STAMP)
	 $(RELEASE_STAMP) -p opentheory doc/*.html src/Tool.sml

.PHONY: documentation
documentation:

.PHONY: tarball
tarball: clean doc/DONT-RELEASE Makefile.dev
	cd .. ; COPYFILE_DISABLE=true tar cvzhf opentheory/release/opentheory.tar.gz --exclude-from opentheory/doc/DONT-RELEASE opentheory

.PHONY: release-instructions
release-instructions:
	@echo "==============================================================="
	@echo "Completed release, now do the following:"
	@echo "1. git add, commit and push all changes"
	@perl -ne 'if ($$_ =~ /^opentheory ([0-9.]+) \(release ([0-9]+)\),$$/) { print "2. git tag -a -s v$$1.$$2 -m \"Version $$1 (release $$2)\"\n"; }' doc/download.html
	@echo "3. git push --tags"
	@echo "4. Browse to github > opentheory > releases > Latest release"
	@echo "5. Add the release name and tarball"
	@echo "==============================================================="

.PHONY: release
release: release-stamp mosml mlton polyml documentation
	rm -f $(RELEASE_DIR)/*.html $(RELEASE_DIR)/*.png
	cp -v doc/*.html doc/*.png $(RELEASE_DIR)/
	cp -v doc/favicon.ico $(RELEASE_DIR)/
	cp -v doc/MIT-LICENSE $(RELEASE_DIR)/
	$(MAKE) tarball
	rsync -azv --delete --checksum --size-only --exclude=.gitignore -e ssh $(RELEASE_DIR)/ joe@login.gilith.com:www/gilith/software/opentheory
	ssh joe@login.gilith.com '/bin/bash -l bin/install-opentheory'
	@if GIT_PAGER='' git grep '[*][*][*]' ; then echo "WARNING: TODO comments discovered" ; fi
	$(MAKE) release-instructions