https://github.com/EasyCrypt/easycrypt
Revision 66c830f9593684da87d07c365a68f1a17156de74 authored by François Dupressoir on 15 June 2020, 14:55:33 UTC, committed by François Dupressoir on 15 June 2020, 14:55:33 UTC
Now reduced to PROM as core, with ROM as a simpler interface. PROM is concrete to allow reuse of its flag type. Its internal theories, and ROM, are abstract to avoid growing forests of clones when using eager arguments. ROM now aligns with PROM in cloning interface: additional types `d_in_t` and `d_out_t` specify the distinguisher's interface. (This simplifies instantiation.) Some changes to type and oracle names to make them more explicit. Notably: - `from` is now `in_t`, - `to` is now `out_t`, (with associated change on name of distribution).
1 parent 734e5bb
Tip revision: 66c830f9593684da87d07c365a68f1a17156de74 authored by François Dupressoir on 15 June 2020, 14:55:33 UTC
Clean up the ROM libraries
Clean up the ROM libraries
Tip revision: 66c830f
Makefile
# -*- Makefile -*-
# --------------------------------------------------------------------
OCAMLBUILD_JOBS ?= 1
OCAMLBUILD_BIN ?= ocamlbuild
OCAMLBUILD_EXTRA ?=
OCAMLBUILD_OPTS := -use-ocamlfind -j $(OCAMLBUILD_JOBS)
# In Emacs, use classic display to enable error jumping.
ifeq ($(shell echo $$TERM), dumb)
OCAMLBUILD_OPTS += -classic-display
endif
ifeq ($(LINT),1)
OCAMLBUILD_OPTS += -tag lint
endif
OCAMLBUILD_OPTS += $(OCAMLBUILD_EXTRA)
OCAMLBUILD := $(OCAMLBUILD_BIN) $(OCAMLBUILD_OPTS)
DESTDIR ?=
PREFIX ?= /usr/local
VERSION ?= $(shell date '+%F')
DISTDIR := easycrypt-$(VERSION)
INSTALL := scripts/install/install-sh
PWD := $(shell pwd)
COMMIT := $(shell scripts/install/get-commit)
FVERSION := src/ecVersion.ml
include Makefile.system
# --------------------------------------------------------------------
BINDIR := $(PREFIX)/bin
LIBDIR := $(PREFIX)/lib/easycrypt
SHRDIR := $(PREFIX)/share/easycrypt
# --------------------------------------------------------------------
ECARGS ?=
ECTOUT ?= 10
ECJOBS ?= 1
ECEXTRA ?= --report=report.log
ECPROVERS ?= Alt-Ergo Z3 CVC4
CHECKPY ?=
CHECK := $(CHECKPY) scripts/testing/runtest
CHECK += --bin-args="$(ECARGS)" --bin-args="$(ECPROVERS:%=-p %)"
CHECK += --timeout="$(ECTOUT)" --jobs="$(ECJOBS)"
CHECK += $(ECEXTRA) config/tests.config
CHECKCATS ?= prelude stdlib
# --------------------------------------------------------------------
.PHONY: all build byte native tests check weak-check examples
.PHONY: clean install uninstall uninstall-purge dist distcheck
.PHONY: license
.PHONY: %.ml %.mli %.inferred.mli
all: build
@true
build: native
define do-core-build
$(OCAMLBUILD) "$(1)"
endef
define do-build
rm -f "$(1)$(EXE)"
sed 's/COMMIT/$(COMMIT)/g' < $(FVERSION).in > $(FVERSION)
$(call do-core-build,src/$(1))
if [ ! -z "$(EXE)" ]; then \
cp "_build/src/$(1)" "$(1)$(EXE)"; \
fi
endef
byte:
$(call do-build,ec.byte)
native:
$(call do-build,ec.native)
define check-for-staled-files
if [ -d "$(DESTDIR)$(PREFIX)/lib/easycrypt/" ]; then \
cd "$(DESTDIR)$(LIBDIR)/" && \
find theories -type f -name '*.ec*' 2>/dev/null | \
sed 's/^/!! FOUND STALED FILE: /'; \
fi
endef
install: build uninstall
-@$(call check-for-staled-files)
$(INSTALL) -m 0755 -d $(DESTDIR)$(BINDIR)
$(INSTALL) -m 0755 -T ec.native $(DESTDIR)$(BINDIR)/easycrypt$(EXE)
$(INSTALL) -m 0755 -T scripts/testing/runtest $(DESTDIR)$(BINDIR)/ec-runtest$(EXE)
for i in $$(find theories -type d -mindepth 1); do \
$(INSTALL) -m 0755 -d $(DESTDIR)$(LIBDIR)/$$i ';'; \
$(INSTALL) -m 0644 -t $(DESTDIR)$(LIBDIR)/$$i $$i/*.ec*; \
done
define rmdir
-@if [ -d "$(1)" ]; then rmdir "$(1)"; fi
endef
uninstall:
rm -f $(DESTDIR)$(BINDIR)/easycrypt
for i in $$(find theories -depth -type d); do \
for j in $$i/*.ec*; do rm -f $(DESTDIR)$(LIBDIR)/$$j; done; \
rmdir $(DESTDIR)$(LIBDIR)/$$i 2>/dev/null || true; \
done
rm -f $(DESTDIR)$(SHRDIR)/emacs/*.el
$(call rmdir,$(DESTDIR)$(SHRDIR)/emacs)
$(call rmdir,$(DESTDIR)$(SHRDIR))
uninstall-purge:
rm -f $(DESTDIR)$(BINDIR)/easycrypt
rm -rf $(DESTDIR)$(LIBDIR)
rm -rf $(DESTDIR)$(SHRDIR)
tests: check
examples: build
$(CHECK) examples mee-cbc
check: build
$(CHECK) $(CHECKCATS)
weak-check: build
$(CHECK) --bin-args="-pragmas Proofs:weak" $(CHECKCATS) '!unit'
license:
scripts/srctx/license COPYRIGHT.yaml \
$(shell find src -name '*.ml' -o -name '*.ml[a-z]') \
$(shell find theories -name '*.ec' -o -name '*.ec[a-z]') \
$(shell find proofgeneral/easycrypt -name '*.el')
clean:
$(OCAMLBUILD) -clean
rm -f ec.native ec.byte
rm -f ec.native.exe ec.byte.exe
find theories examples -name '*.eco' -exec rm '{}' ';'
# --------------------------------------------------------------------
dist:
if [ -e $(DISTDIR) ]; then rm -rf $(DISTDIR); fi
./scripts/install/distribution $(DISTDIR) MANIFEST
BZIP2=-9 $(TAR) -cjf $(DISTDIR).tar.bz2 --owner=0 --group=0 $(DISTDIR)
rm -rf $(DISTDIR)
distcheck: dist
$(TAR) -xof $(DISTDIR).tar.bz2
set -x; \
$(MAKE) -C $(DISTDIR) \
&& $(MAKE) -C $(DISTDIR) dist \
&& mkdir $(DISTDIR)/dist1 $(DISTDIR)/dist2 \
&& ( cd $(DISTDIR)/dist1 && $(TAR) -xof ../$(DISTDIR).tar.bz2 ) \
&& ( cd $(DISTDIR)/dist2 && $(TAR) -xof ../../$(DISTDIR).tar.bz2 ) \
&& diff -rq $(DISTDIR)/dist1 $(DISTDIR)/dist2 \
|| exit 1
rm -rf $(DISTDIR)
@echo "$(DISTDIR) is ready for distribution" | \
sed -e 1h -e 1s/./=/g -e 1p -e 1x -e '$$p' -e '$$x'
# --------------------------------------------------------------------
%.inferred.mli:
@$(call do-core-build,src/$@) && cat _build/src/$@
# --------------------------------------------------------------------
%.ml:
$(call do-core-build,src/$*.cmo)
# --------------------------------------------------------------------
%.mli:
$(call do-core-build,src/$*.cmi)
Computing file changes ...