Skip to content

Commit

Permalink
Prepare for 1.4
Browse files Browse the repository at this point in the history
  • Loading branch information
@abentkamp
abentkamp committed Dec 8, 2017
1 parent 02a90ba commit e5250fa
Show file tree
Hide file tree
Showing 6 changed files with 176 additions and 15 deletions.
2 changes: 1 addition & 1 deletion _oasis
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
OASISFormat: 0.4
Name: zipperposition
Version: 1.3
Version: 1.4
Homepage: https://github.com/c-cube/zipperposition
Authors: Simon Cruanes
License: BSD-3-clause
Expand Down
11 changes: 10 additions & 1 deletion _tags
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
# OASIS_START
# DO NOT EDIT (digest: 54a0603eb7e995d81154db0521e15702)
# DO NOT EDIT (digest: bf0e9b4542a1ebdd9122f6807c0f025f)
# Ignore VCS directories, you can use the same kind of rule outside
# OASIS_START/STOP if you want to exclude directories that contains
# useless stuff for the build process
Expand Down Expand Up @@ -359,6 +359,15 @@ true: annot, bin_annot
"src/tools/cnf_of.native": package(zarith)
"src/tools/cnf_of.native": use_logtk
"src/tools/cnf_of.native": use_logtk_parsers
# Executable app_encode
"src/tools/app_encode.native": package(bytes)
"src/tools/app_encode.native": package(containers)
"src/tools/app_encode.native": package(containers.data)
"src/tools/app_encode.native": package(sequence)
"src/tools/app_encode.native": package(unix)
"src/tools/app_encode.native": package(zarith)
"src/tools/app_encode.native": use_logtk
"src/tools/app_encode.native": use_logtk_parsers
# Executable tptp_to_zf
"src/tools/tptp_to_zf.native": package(bytes)
"src/tools/tptp_to_zf.native": package(containers)
Expand Down
2 changes: 1 addition & 1 deletion opam
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
opam-version: "1.2"
name: "zipperposition"
version: "1.3"
version: "1.4"
maintainer: "simon.cruanes@inria.fr"
author: "Simon Cruanes"
homepage: "https://github.com/c-cube/zipperposition"
Expand Down
160 changes: 156 additions & 4 deletions setup.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(* setup.ml generated for the first time by OASIS v0.4.4 *)

(* OASIS_START *)
(* DO NOT EDIT (digest: d4189afb0ba9a73f260ed1393daf55c0) *)
(* DO NOT EDIT (digest: e674214876b4d7ef36b78560efd40297) *)
(*
Regenerated by OASIS v0.4.10
Visit http://oasis.forge.ocamlcore.org for more information and
Expand Down Expand Up @@ -7103,7 +7103,7 @@ let setup_t =
{
oasis_version = "0.4";
ocaml_version = Some (OASISVersion.VGreaterEqual "4.00.1");
version = "1.3";
version = "1.4";
license =
OASISLicense.DEP5License
(OASISLicense.DEP5Unit
Expand Down Expand Up @@ -9428,6 +9428,158 @@ let setup_t =
bs_nativeopt = [(OASISExpr.EBool true, [])]
},
{exec_custom = false; exec_main_is = "cnf_of.ml"});
Executable
({
cs_name = "app_encode";
cs_data = PropList.Data.create ();
cs_plugin_data = []
},
{
bs_build =
[
(OASISExpr.EBool true, false);
(OASISExpr.EAnd
(OASISExpr.EFlag "tools",
OASISExpr.EFlag "parsers"),
true)
];
bs_install =
[
(OASISExpr.EBool true, false);
(OASISExpr.EAnd
(OASISExpr.EFlag "tools",
OASISExpr.EFlag "parsers"),
true)
];
bs_path = "src/tools/";
bs_compiled_object = Native;
bs_build_depends =
[
InternalLibrary "logtk";
InternalLibrary "logtk_parsers"
];
bs_build_tools = [ExternalTool "ocamlbuild"];
bs_interface_patterns =
[
{
OASISSourcePatterns.Templater.atoms =
[
OASISSourcePatterns.Templater.Text "";
OASISSourcePatterns.Templater.Expr
(OASISSourcePatterns.Templater.Call
("capitalize_file",
OASISSourcePatterns.Templater.Ident
"module"));
OASISSourcePatterns.Templater.Text ".mli"
];
origin = "${capitalize_file module}.mli"
};
{
OASISSourcePatterns.Templater.atoms =
[
OASISSourcePatterns.Templater.Text "";
OASISSourcePatterns.Templater.Expr
(OASISSourcePatterns.Templater.Call
("uncapitalize_file",
OASISSourcePatterns.Templater.Ident
"module"));
OASISSourcePatterns.Templater.Text ".mli"
];
origin = "${uncapitalize_file module}.mli"
}
];
bs_implementation_patterns =
[
{
OASISSourcePatterns.Templater.atoms =
[
OASISSourcePatterns.Templater.Text "";
OASISSourcePatterns.Templater.Expr
(OASISSourcePatterns.Templater.Call
("capitalize_file",
OASISSourcePatterns.Templater.Ident
"module"));
OASISSourcePatterns.Templater.Text ".ml"
];
origin = "${capitalize_file module}.ml"
};
{
OASISSourcePatterns.Templater.atoms =
[
OASISSourcePatterns.Templater.Text "";
OASISSourcePatterns.Templater.Expr
(OASISSourcePatterns.Templater.Call
("uncapitalize_file",
OASISSourcePatterns.Templater.Ident
"module"));
OASISSourcePatterns.Templater.Text ".ml"
];
origin = "${uncapitalize_file module}.ml"
};
{
OASISSourcePatterns.Templater.atoms =
[
OASISSourcePatterns.Templater.Text "";
OASISSourcePatterns.Templater.Expr
(OASISSourcePatterns.Templater.Call
("capitalize_file",
OASISSourcePatterns.Templater.Ident
"module"));
OASISSourcePatterns.Templater.Text ".mll"
];
origin = "${capitalize_file module}.mll"
};
{
OASISSourcePatterns.Templater.atoms =
[
OASISSourcePatterns.Templater.Text "";
OASISSourcePatterns.Templater.Expr
(OASISSourcePatterns.Templater.Call
("uncapitalize_file",
OASISSourcePatterns.Templater.Ident
"module"));
OASISSourcePatterns.Templater.Text ".mll"
];
origin = "${uncapitalize_file module}.mll"
};
{
OASISSourcePatterns.Templater.atoms =
[
OASISSourcePatterns.Templater.Text "";
OASISSourcePatterns.Templater.Expr
(OASISSourcePatterns.Templater.Call
("capitalize_file",
OASISSourcePatterns.Templater.Ident
"module"));
OASISSourcePatterns.Templater.Text ".mly"
];
origin = "${capitalize_file module}.mly"
};
{
OASISSourcePatterns.Templater.atoms =
[
OASISSourcePatterns.Templater.Text "";
OASISSourcePatterns.Templater.Expr
(OASISSourcePatterns.Templater.Call
("uncapitalize_file",
OASISSourcePatterns.Templater.Ident
"module"));
OASISSourcePatterns.Templater.Text ".mly"
];
origin = "${uncapitalize_file module}.mly"
}
];
bs_c_sources = [];
bs_data_files = [];
bs_findlib_extra_files = [];
bs_ccopt = [(OASISExpr.EBool true, [])];
bs_cclib = [(OASISExpr.EBool true, [])];
bs_dlllib = [(OASISExpr.EBool true, [])];
bs_dllpath = [(OASISExpr.EBool true, [])];
bs_byteopt = [(OASISExpr.EBool true, [])];
bs_nativeopt = [(OASISExpr.EBool true, [])]
},
{exec_custom = false; exec_main_is = "app_encode.ml"});
Executable
({
cs_name = "tptp_to_zf";
Expand Down Expand Up @@ -9940,15 +10092,15 @@ let setup_t =
};
oasis_fn = Some "_oasis";
oasis_version = "0.4.10";
oasis_digest = Some "\244\225\240l\202\178\188\162\211\187\252pPs{-";
oasis_digest = Some "u[\236\180b\235\142J\167#\222Y0\nn\211";
oasis_exec = None;
oasis_setup_args = [];
setup_update = false
};;

let setup () = BaseSetup.setup setup_t;;

# 9952 "setup.ml"
# 10104 "setup.ml"
let setup_t = BaseCompat.Compat_0_4.adapt_setup_t setup_t
open BaseCompat.Compat_0_4
(* OASIS_STOP *)
Expand Down
12 changes: 6 additions & 6 deletions src/core/META
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# OASIS_START
# DO NOT EDIT (digest: 2a1233420419c19f052a5a15d28754db)
version = "1.3"
# DO NOT EDIT (digest: e404fb6f07299c42c89a2c73a5ca8582)
version = "1.4"
description =
"Superposition theorem prover, for first order logic with equality."
requires = "zarith unix sequence containers containers.data bytes"
Expand All @@ -10,7 +10,7 @@ archive(native) = "logtk.cmxa"
archive(native, plugin) = "logtk.cmxs"
exists_if = "logtk.cma"
package "solving" (
version = "1.3"
version = "1.4"
description =
"Superposition theorem prover, for first order logic with equality."
requires = "logtk msat"
Expand All @@ -22,7 +22,7 @@ package "solving" (
)

package "proofs" (
version = "1.3"
version = "1.4"
description =
"Superposition theorem prover, for first order logic with equality."
requires = "logtk"
Expand All @@ -34,7 +34,7 @@ package "proofs" (
)

package "parsers" (
version = "1.3"
version = "1.4"
description =
"Superposition theorem prover, for first order logic with equality."
requires = "logtk"
Expand All @@ -46,7 +46,7 @@ package "parsers" (
)

package "arbitrary" (
version = "1.3"
version = "1.4"
description =
"Superposition theorem prover, for first order logic with equality."
requires = "logtk qcheck"
Expand Down
4 changes: 2 additions & 2 deletions src/prover/META
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# OASIS_START
# DO NOT EDIT (digest: a6109529443f3b9eeca5bbde2852a862)
version = "1.3"
# DO NOT EDIT (digest: d146e3a82931b52f33abefa94674eaa7)
version = "1.4"
description =
"Superposition theorem prover, for first order logic with equality."
requires =
Expand Down

0 comments on commit e5250fa

Please sign in to comment.