Merge branch 'master' into stable for 1.5

.dockerignore

@@ -0,0 +1,3 @@
+.git
+examples
+_build

.gitignore

@@ -38,3 +38,5 @@ setup.*
 examples
 benchs
 *.exe
+*.install
+.merlin

CHANGELOG.md

@@ -1,5 +1,75 @@
 # Changelog
 
+## 1.5
+
+- be compatible with sequence >= 1.0
+- cli option to switch off maximal number of variables per clause
+- Dockerfile and instructions to build a docker image
+- add eta-reduction to `LLTerm`
+- update phases API + params so it's easier to use from utop
+- move to jbuilder
+
+- fail early when unifying a variable and a polymorphic constant
+- More realistic test to expose a bug in unification of polymorphic terms
+- upper bound on msat and deps on logtk
+- fix for llprover (use congruence correctly for poly equalities)
+- printer for congruence
+- cache llproof checking result, display it in llproof-printing
+- refactor proof checker to look more like a tableaux prover + dot printing
+- llprover: hack to allow checking of rewriting steps that occur under binders
+- split proof checker into its own module `LLProver`
+- add linear expressions and arith predicates in `LLTerm`
+- make demodulation more robust
+- bugfix in `Type.apply` for polymorphic type arguments
+- stop positive extensionality rule from removing type arguments
+- moved detection for "distinct object" syntax into TypeInference
+- omit type declarations for distinct objects in TPTP output
+- bugfix restrict_to_scope: recursive call when variable already in scope
+- bugfix: type of polymorphic application in app_encode tool
+- bugfix: app_encode extensionality axiom needs type arguments
+- `fo_detector` tool to count problems with applied variables
+- clean up Subst module
+- bugfix: wrong polymorphic types in returned unifier
+- remove hornet from makefile, improve logitest targets
+- remove hornet
+- better type error messages
+- make `Subst.apply` tailrec
+- "int" mode for variable purification
+- bugfix: unquote identifiers in TPTP parser
+
+## 1.4
+
+- remove inlining on parsers
+- cli option for ext-neg rule
+- add `--check-types` for checking types deeply in new clauses
+- Add ExistsConst (??) and ForallConst (!!) to TPTP parser
+- TPTP parser: allow function types as THF terms
+- add cli option `-bt` (alias to `--backtraces`)
+- completion of equalities with λ-abstractions as RHS in type inference
+- THF parser: allow for `@` applications in types
+- cli flag for ext_pos
+- App encode: binary for app-encoding HO applications into FO
+
+- bugfix in ho unification
+- in unification, fix order in which bound variables are added to env
+- bugfix in unification (would produce wrong type)
+- do not simplify in demodulation
+- Add StarExec instructions to readme
+- bugfixes `app_encode`
+- β-normalize rewrite rules that are eq-completed
+- uniform output of “SZS status” instead of “SZS Status”
+- auto flattening of applications in STerm
+- fix `examples/ho/extensionality1.zf` by forbidding some HO demodulations
+- fix tag managing (and therefore proof checking) for `Lit.is_absurd`
+- bugfix in proof checking related to instantiation
+- bugfix in NPDtree
+- more elegant and robust sup-at-var condition
+- sup-at-var condition with polymorphism
+- remove literal comparison by constraint
+- no selection of literals containing ho variables
+- Stricter sup-at-vars condition
+- purify naked variables
+
 ## 1.3
 
 - experimental proof checking with `--check` (and `--dot-llproof <file>`)

Dockerfile

@@ -0,0 +1,21 @@
+FROM ocaml/opam:alpine as build
+# init and set perms
+WORKDIR /zipper/build
+RUN sudo chown opam: /zipper/build
+# deps
+RUN eval `opam config env` && \
+    opam update && \
+    opam depext -i zarith && \
+    opam install jbuilder zarith containers sequence msat menhir
+# main build
+COPY --chown=opam:nogroup src *.opam Makefile ./
+RUN eval `opam config env` && \
+    make build && \
+    cp _build/default/main/zipperposition.exe ./zipperposition
+
+# prepare lightweight production image
+FROM alpine:latest as prod
+WORKDIR /root
+RUN apk update && apk add gmp-dev
+COPY --from=build /zipper/build/zipperposition .
+ENTRYPOINT ["./zipperposition"]