diff --git a/.gitignore b/.gitignore index e139737..7da3b50 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,2 @@ /alt-ergo-icons.tar.xz -/alt-ergo-0.99.1.tar.gz -/alt-ergo-1.01.tar.gz -/alt-ergo-1.30.tar.gz +/alt-ergo-*.tar.gz diff --git a/README.md b/README.md new file mode 100644 index 0000000..fa65fbb --- /dev/null +++ b/README.md @@ -0,0 +1,9 @@ +# alt-ergo + +[Alt-Ergo](https://alt-ergo.ocamlpro.com/) is an automated theorem prover +implemented in OCaml. It is based on `CC(X)` — a congruence closure +algorithm parameterized by an equational theory X. This algorithm is +reminiscent of the Shostak algorithm. Currently `CC(X)` is instantiated by +the theory of linear arithmetics. Alt-Ergo also contains a home made +SAT-solver and an instantiation mechanism by which it fully supports +quantifiers. diff --git a/alt-ergo-1.30-use-pic.patch b/alt-ergo-1.30-use-pic.patch deleted file mode 100644 index 71d6ad0..0000000 --- a/alt-ergo-1.30-use-pic.patch +++ /dev/null @@ -1,19 +0,0 @@ ---- alt-ergo-1.30.old/Makefile.users 2017-11-09 09:55:47.337871409 +0000 -+++ alt-ergo-1.30/Makefile.users 2017-11-09 10:00:52.374639872 +0000 -@@ -140,14 +140,14 @@ - $(OCAMLC) $(BFLAGS) -o $@ $(BIBBYTE) $^ - - $(NAME).opt: $(MAINCMX) -- $(OCAMLOPT) $(OFLAGS) -o $@ $(BIBOPT) $^ -+ $(OCAMLOPT) $(OFLAGS) -runtime-variant _pic -o $@ $(BIBOPT) $^ - - #### - $(GUINAME).byte: $(GUICMO) - $(OCAMLC) $(BFLAGS) -o $(GUINAME).byte $(BIBBYTE) $(BIBGUIBYTE) $^ - - $(GUINAME).opt: $(GUICMX) -- $(OCAMLOPT) $(OFLAGS) -o $(GUINAME).opt $(BIBOPT) $(BIBGUIOPT) $^ -+ $(OCAMLOPT) $(OFLAGS) -runtime-variant _pic -o $(GUINAME).opt $(BIBOPT) $(BIBGUIOPT) $^ - - ifeq ($(ENABLEGUI),yes) - gui: $(GUINAME).$(OCAMLBEST) diff --git a/alt-ergo-dune3.patch b/alt-ergo-dune3.patch new file mode 100644 index 0000000..cb875a4 --- /dev/null +++ b/alt-ergo-dune3.patch @@ -0,0 +1,29 @@ +--- alt-ergo-2.3.0-free/sources/configure.ml.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/configure.ml 2022-07-05 16:42:35.856375154 -0600 +@@ -139,26 +139,6 @@ let () = + Format.eprintf "ERROR: Couldn't find dune in env@."; + exit 1 + +-(* run dune to check that dependencies are installed *) +-let () = +- let p_opt = match !pkg with +- | "" -> "" +- | s -> Format.asprintf "-p %s" s +- in +- let cmd = Format.asprintf +- "dune external-lib-deps --display=quiet --missing %s @install" +- p_opt +- in +- let ch = Unix.open_process_in cmd in +- let _ = read_all ch in +- let res = Unix.close_process_in ch in +- match res with +- | Unix.WEXITED 0 -> +- Format.printf "All deps are installed.@." +- | _ -> +- (* dune already prints the missing libs on stderr *) +- exit 2 +- + let () = + Format.printf "Good to go !@." + diff --git a/alt-ergo-forward-compat.patch b/alt-ergo-forward-compat.patch new file mode 100644 index 0000000..b3be679 --- /dev/null +++ b/alt-ergo-forward-compat.patch @@ -0,0 +1,64 @@ +--- alt-ergo-2.3.0-free/sources/alt-ergo-lib-free.opam.orig 2022-05-20 03:15:57.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/alt-ergo-lib-free.opam 2022-07-05 16:40:03.983955825 -0600 +@@ -15,8 +15,6 @@ depends: [ + "num" + "ocplib-simplex" {>= "0.4" } + "zarith" +- "seq" +- "stdlib-shims" + ] + conflicts: [ + "alt-ergo" +--- alt-ergo-2.3.0-free/sources/alt-ergo-lib.opam.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/alt-ergo-lib.opam 2022-07-05 16:47:56.113259397 -0600 +@@ -15,8 +15,6 @@ depends: [ + "num" + "ocplib-simplex" {>= "0.4" } + "zarith" +- "seq" +- "stdlib-shims" + ] + conflicts: [ + "alt-ergo-free" +--- alt-ergo-2.3.0-free/sources/alt-ergo-parsers-free.opam.orig 2022-05-20 03:16:01.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/alt-ergo-parsers-free.opam 2022-06-18 16:35:52.177624279 -0600 +@@ -16,7 +16,6 @@ depends: [ + "psmt2-frontend" { >= "0.2" & < "0.4" } + "camlzip" + "menhir" { < "20210310" } +- "stdlib-shims" + ] + conflicts: [ + "alt-ergo-parsers" +--- alt-ergo-2.3.0-free/sources/alt-ergo-parsers.opam.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/alt-ergo-parsers.opam 2022-07-05 16:39:33.254870985 -0600 +@@ -16,7 +16,6 @@ depends: [ + "psmt2-frontend" { >= "0.2" } + "camlzip" + "menhir" +- "stdlib-shims" + ] + homepage: "http://alt-ergo.ocamlpro.com/" + dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git" +--- alt-ergo-2.3.0-free/sources/lib/dune.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/dune 2022-07-05 16:50:35.778700249 -0600 +@@ -9,7 +9,7 @@ + (public_name alt-ergo-lib) + + ; external dependencies +- (libraries seq unix num str zarith dynlink ocplib-simplex stdlib-shims) ++ (libraries unix num str zarith dynlink ocplib-simplex) + + ; .mli only modules *also* need to be in this field + (modules_without_implementation matching_types numbersInterface sig sig_rel) +--- alt-ergo-2.3.0-free/sources/parsers/dune.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/parsers/dune 2022-06-18 16:36:07.177661183 -0600 +@@ -14,7 +14,7 @@ + (library + (name AltErgoParsers) + (public_name alt-ergo-parsers) +- (libraries camlzip dynlink psmt2-frontend alt-ergo-lib stdlib-shims) ++ (libraries camlzip dynlink psmt2-frontend alt-ergo-lib) + (modules + ; common + Parsers Parsers_loader MyZip diff --git a/alt-ergo-inline-error.patch b/alt-ergo-inline-error.patch new file mode 100644 index 0000000..ccb8356 --- /dev/null +++ b/alt-ergo-inline-error.patch @@ -0,0 +1,26 @@ +Fixes these errors: + +File "lib/util/util.mli", line 62, characters 6-12: +62 | val [@inline always] compare_algebraic : 'a -> 'a -> (('a * 'a) -> int) -> int + ^^^^^^ +Error (warning 53 [misplaced-attribute]): the "inline" attribute cannot appear in this context + +File "lib/util/util.mli", line 64, characters 6-12: +64 | val [@inline always] cmp_lists: 'a list -> 'a list -> ('a -> 'a -> int) -> int + ^^^^^^ +Error (warning 53 [misplaced-attribute]): the "inline" attribute cannot appear in this context + +--- alt-ergo-2.3.0-free/sources/lib/util/util.mli.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/lib/util/util.mli 2024-05-05 11:41:32.415674847 -0600 +@@ -59,9 +59,9 @@ val string_of_th_ext : theories_extensio + - Pervasives.compare a b is used if + + *) +-val [@inline always] compare_algebraic : 'a -> 'a -> (('a * 'a) -> int) -> int ++val compare_algebraic : 'a -> 'a -> (('a * 'a) -> int) -> int + +-val [@inline always] cmp_lists: 'a list -> 'a list -> ('a -> 'a -> int) -> int ++val cmp_lists: 'a list -> 'a list -> ('a -> 'a -> int) -> int + + type matching_env = + { diff --git a/alt-ergo-menhir.patch b/alt-ergo-menhir.patch new file mode 100644 index 0000000..4ab3e45 --- /dev/null +++ b/alt-ergo-menhir.patch @@ -0,0 +1,18 @@ +--- alt-ergo-2.3.0-free/sources/plugins/AB-Why3/dune.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/plugins/AB-Why3/dune 2022-06-20 13:27:36.662944620 -0600 +@@ -3,13 +3,13 @@ + + (menhir + (infer false) +- (flags --fixed-exception) ++ (flags --fixed-exception --table) + (modules why3_parser) + ) + + (library + (name ABWhy3Plugin) +- (libraries alt-ergo-lib alt-ergo-parsers) ++ (libraries alt-ergo-lib alt-ergo-parsers menhirLib) + (modules Why3_lexer Why3_parser Why3_loc Why3_ptree) + ) + diff --git a/alt-ergo-pervasives.patch b/alt-ergo-pervasives.patch new file mode 100644 index 0000000..bd72f54 --- /dev/null +++ b/alt-ergo-pervasives.patch @@ -0,0 +1,172 @@ +--- alt-ergo-2.3.0-free/extra/ocpChecker.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/extra/ocpChecker.ml 2022-02-23 12:58:05.976390283 -0700 +@@ -45,10 +45,10 @@ let update_file file lines = + exit 2 + in + Queue.iter (fun line -> +- Pervasives.output_string cout line; +- Pervasives.output_string cout "\n" ++ Stdlib.output_string cout line; ++ Stdlib.output_string cout "\n" + )lines; +- Pervasives.flush cout; ++ Stdlib.flush cout; + close_out cout + + +--- alt-ergo-2.3.0-free/sources/tools/gui/annoted_ast.ml.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/tools/gui/annoted_ast.ml 2022-06-18 16:08:13.053310654 -0600 +@@ -191,7 +191,7 @@ type annoted_node = + module MDep = Map.Make ( + struct + type t = atyped_decl annoted +- let compare = Pervasives.compare ++ let compare = Stdlib.compare + end) + + +@@ -880,9 +880,9 @@ let find_dep_by_string dep s = + | None -> begin + match d.c with + | ALogic (_, ls, _, _) when List.mem s ls -> Some d +- | ATypeDecl (_, _, s', _, _) when Pervasives.(=) s s'-> Some d +- | APredicate_def (_, p, _, _) when Pervasives.(=) s p -> Some d +- | AFunction_def (_, f, _, _, _, _) when Pervasives.(=) s f -> Some d ++ | ATypeDecl (_, _, s', _, _) when Stdlib.(=) s s'-> Some d ++ | APredicate_def (_, p, _, _) when Stdlib.(=) s p -> Some d ++ | AFunction_def (_, f, _, _, _, _) when Stdlib.(=) s f -> Some d + | _ -> None + end + ) dep None +@@ -892,7 +892,7 @@ let find_tag_deps dep tag = + (fun d (deps,_) found -> + match found with + | Some _ -> found +- | None -> if Pervasives.(=) d.tag tag then Some deps else None ++ | None -> if Stdlib.(=) d.tag tag then Some deps else None + ) dep None + + let find_tag_inversedeps dep tag = +@@ -900,7 +900,7 @@ let find_tag_inversedeps dep tag = + (fun d (_,deps) found -> + match found with + | Some _ -> found +- | None -> if Pervasives.(=) d.tag tag then Some deps else None ++ | None -> if Stdlib.(=) d.tag tag then Some deps else None + ) dep None + + let make_dep_string d ex dep s = +@@ -2046,7 +2046,7 @@ and findtags_aform sl aform acc = + (fun sl (sy, _) -> + let s = Symbols.to_string_clean sy in + List.fold_left +- (fun l s' -> if Pervasives.(=) s' s then l else s'::l) [] sl ++ (fun l s' -> if Stdlib.(=) s' s then l else s'::l) [] sl + )sl l + in + findtags_aform sl aaf.c acc +--- alt-ergo-2.3.0-free/sources/tools/gui/connected_ast.ml.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/tools/gui/connected_ast.ml 2022-06-18 16:08:37.469375133 -0600 +@@ -388,7 +388,7 @@ let rec unquantify_aform (buffer:sbuffer + List.fold_left (fun (nbv, used, goal_used, ve, uplet, lets) v -> + let ((s, _) as v'), e = List.hd ve in + let cdr_ve = List.tl ve in +- assert (Pervasives.(=) v v'); ++ assert (Stdlib.(=) v v'); + if String.length e == 0 then + (v'::nbv, used, goal_used, cdr_ve, v'::uplet, lets) + else +@@ -545,7 +545,7 @@ let rec add_instance_aux ?(register=true + make_instance env.inst_buffer vars entries af goal_form tyenv in + let ln_form = least_nested_form used_vars goal_form in + env.inst_buffer#place_cursor ~where:env.inst_buffer#end_iter; +- if Pervasives.(=) ln_form (Exists goal_form) then begin ++ if Stdlib.(=) ln_form (Exists goal_form) then begin + let hy = + AAxiom (loc, (sprintf "%s%s" "_instance_" aname), ax_kd, instance.c) in + let ahy = new_annot env.inst_buffer hy instance.id ptag in +@@ -739,7 +739,7 @@ and add_trigger ?(register=true) t qid e + if register then + save env.actions + (AddTrigger (qf.id, +- Pervasives.(=) sbuf env.inst_buffer, str)); ++ Stdlib.(=) sbuf env.inst_buffer, str)); + commit_tags_buffer sbuf + | _ -> assert false + end +--- alt-ergo-2.3.0-free/sources/tools/gui/main_gui.ml.orig 2022-05-20 01:34:55.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/tools/gui/main_gui.ml 2022-06-18 16:09:14.324472461 -0600 +@@ -151,7 +151,7 @@ let save_session envs = + + let save_dialog cancel envs () = + if List.exists +- (fun env -> Pervasives.(<>) env.actions env.saved_actions) envs then ++ (fun env -> Stdlib.(<>) env.actions env.saved_actions) envs then + if List.exists + (fun env -> not (Gui_session.safe_session env.actions)) envs then + GToolbox.message_box +@@ -250,7 +250,7 @@ let pop_model sat_env () = + let compare_rows icol_number (model:#GTree.model) row1 row2 = + let t1 = model#get ~row:row1 ~column:icol_number in + let t2 = model#get ~row:row2 ~column:icol_number in +- Pervasives.compare t1 t2 ++ Stdlib.compare t1 t2 + + + let empty_inst_model () = +@@ -382,7 +382,7 @@ let refresh_timers t () = + let total = + tsat +. tmatch +. tcc +. tarith +. tarrays +. tsum +. trecords +. tac in + +- let total = if Pervasives.(=) total 0. then 1. else total in ++ let total = if Stdlib.(=) total 0. then 1. else total in + + t.tl_sat#set_text (sprintf "%3.2f s" tsat); + t.tl_match#set_text (sprintf "%3.2f s" tmatch); +@@ -455,7 +455,7 @@ let add_inst ({ h; _ } as inst_model) or + let id = Expr.id orig in + let name = + match Expr.form_view orig with +- | Expr.Lemma { Expr.name = n ; _ } when Pervasives.(<>) n "" -> n ++ | Expr.Lemma { Expr.name = n ; _ } when Stdlib.(<>) n "" -> n + | Expr.Lemma _ | Expr.Unit _ | Expr.Clause _ | Expr.Literal _ + | Expr.Skolem _ | Expr.Let _ | Expr.Iff _ | Expr.Xor _ -> + string_of_int id +@@ -607,7 +607,7 @@ let vt_signal = + + let force_interrupt old_action_ref n = + (* This function is called just before the thread's timeslice ends *) +- if Pervasives.(=) (Some (Thread.id(Thread.self()))) !interrupt then ++ if Stdlib.(=) (Some (Thread.id(Thread.self()))) !interrupt then + raise Abort_thread; + match !old_action_ref with + | Sys.Signal_handle f -> f n +@@ -723,8 +723,8 @@ let remove_context env () = + toggle_prune env td + | AAxiom (_, s, _, _) + when String.length s = 0 || +- (Pervasives.(<>) s.[0] '_' && +- Pervasives.(<>) s.[0] '@') -> ++ (Stdlib.(<>) s.[0] '_' && ++ Stdlib.(<>) s.[0] '@') -> + toggle_prune env td + | _ -> () + ) env.ast +@@ -951,7 +951,7 @@ let search_all entry (_sv:GSourceView2.s + buf#remove_tag found_all_tag ~start:buf#start_iter ~stop:buf#end_iter; + let str = entry#text in + let iter = ref buf#start_iter in +- if Pervasives.(<>) str "" then ++ if Stdlib.(<>) str "" then + let result = ref None in + search_one buf str result iter found_all_tag; + while !result != None do +@@ -1300,7 +1300,7 @@ let start_gui all_used_context = + + let set_wrap_lines _ = + List.iter (fun env -> +- if Pervasives.(=) env.goal_view#wrap_mode `NONE then ( ++ if Stdlib.(=) env.goal_view#wrap_mode `NONE then ( + env.goal_view#set_wrap_mode `CHAR; + env.inst_view#set_wrap_mode `CHAR; + Gui_config.update_wrap true diff --git a/alt-ergo-psmt2-frontend.patch b/alt-ergo-psmt2-frontend.patch new file mode 100644 index 0000000..caa9af7 --- /dev/null +++ b/alt-ergo-psmt2-frontend.patch @@ -0,0 +1,12 @@ +--- alt-ergo-2.3.0-free/sources/parsers/psmt2_to_alt_ergo.ml.orig 2021-06-29 06:08:30.000000000 -0600 ++++ alt-ergo-2.3.0-free/sources/parsers/psmt2_to_alt_ergo.ml 2022-02-23 12:59:13.497394356 -0700 +@@ -403,6 +403,9 @@ module Translate = struct + | Cmd_Push _ -> not_supported "push"; assert false + | Cmd_Pop _ -> not_supported "pop"; assert false + | Cmd_Exit -> acc ++ | Cmd_CheckAllSat _ -> not_supported "check-all-sat"; assert false ++ | Cmd_Maximize _ -> not_supported "maximize"; assert false ++ | Cmd_Minimize _ -> not_supported "minimize"; assert false + + let init () = + if Psmt2Frontend.Options.get_is_int_real () then diff --git a/alt-ergo.appdata.xml b/alt-ergo.metainfo.xml similarity index 62% rename from alt-ergo.appdata.xml rename to alt-ergo.metainfo.xml index 145c9a1..cff34da 100644 --- a/alt-ergo.appdata.xml +++ b/alt-ergo.metainfo.xml @@ -1,6 +1,6 @@ - - alt-ergo.desktop + + com.ocamlpro.alt-ergo CC0-1.0 CECILL-C Alt-Ergo @@ -17,13 +17,19 @@ by which it fully supports quantifiers.

+ com.ocamlpro.alt-ergo.desktop - http://jjames.fedorapeople.org/alt-ergo/altgr-ergo-screenshot.png + https://jjames.fedorapeople.org/alt-ergo/altgr-ergo-screenshot.png Basic Alt-Ergo usage - loganjerry@gmail.com - http://alt-ergo.ocamlpro.com/ + alt-ergo-maintainers@fedoraproject.org + https://alt-ergo.ocamlpro.com/ https://github.com/OCamlPro/alt-ergo/issues + https://alt-ergo.ocamlpro.com/#services + + + altgr-ergo + diff --git a/alt-ergo.spec b/alt-ergo.spec index 927f026..3adb6d8 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -1,142 +1,522 @@ +# OCaml packages not built on i686 since OCaml 5 / Fedora 39. +ExcludeArch: %{ix86} + # rpmlint "no-binary" error is not really an error - see: # https://www.redhat.com/archives/fedora-packaging/2008-August/msg00017.html # and ocaml-ocamlgraph spec file for a discussion of this issue. -%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0) -%if !%{opt} -%global debug_package %{nil} -%endif +# The major and minor releases contain a full tarball. Patch releases, however, +# contain only the parts that have changed, typically just the sources +# directory. Use this to set up everything appropriately. +%global minorver 2.3 +%global patchrel 3 Name: alt-ergo -Version: 1.30 -Release: 12%{?dist} +Version: %{minorver}.%{patchrel} +Release: 30%{?dist} Summary: Automated theorem prover including linear arithmetic -License: CeCILL-C -URL: http://alt-ergo.ocamlpro.com/ -Source0: http://alt-ergo.ocamlpro.com/http/%{name}-%{version}/%{name}-%{version}.tar.gz +# The top-level license files apply to the non-free main distribution of +# alt-ergo. The alt-ergo-free distribution, which we package, is distributed +# with the CeCILL-C license, as noted on the website and also in +# sources/tools/gui/main_gui.ml. +# The AB-Why3 plugin is LGPL-2.1-only WITH OCaml-LGPL-linking-exception +License: CECILL-C AND LGPL-2.1-only WITH OCaml-LGPL-linking-exception +URL: https://alt-ergo.ocamlpro.com/ +# The patch releases contain only the sources directory. The other files come +# from the minor releases. +Source0: https://alt-ergo.ocamlpro.com/http/%{name}-free-%{minorver}.0/%{name}-free-%{minorver}.0.tar.gz +%if 0%{?patchrel} > 0 +Source1: https://alt-ergo.ocamlpro.com/http/%{name}-free-%{version}/%{name}-free-%{version}.tar.gz +%endif # Created with gimp from official upstream icon -Source1: %{name}-icons.tar.xz -Source2: %{name}.desktop -Source3: %{name}.appdata.xml - -# Use the asmrun_pic variant when linking the binary. -Patch1: alt-ergo-1.30-use-pic.patch +Source2: %{name}-icons.tar.xz +Source3: %{name}.desktop +Source4: %{name}.metainfo.xml +# Do not use the deprecated Pervasives interface +Patch0: %{name}-pervasives.patch +# Adapt to recent changes in psmt2-frontend +Patch1: %{name}-psmt2-frontend.patch +# Temporarily use the menhir table backend instead of the code backend for the +# AB plugin. Menhir is unable to infer types with the current code and layout. +# Check each new release to see if this is still necessary. +Patch2: %{name}-menhir.patch +# Fedora does not need the forward compatibility seq and stdlib-shims packages +Patch3: %{name}-forward-compat.patch +# Dune 3 eliminated the external-lib-deps command +Patch4: %{name}-dune3.patch +# Avoid errors due to misplaced inline attributes +Patch5: %{name}-inline-error.patch BuildRequires: desktop-file-utils BuildRequires: gtksourceview2-devel -BuildRequires: ocaml -BuildRequires: ocaml-findlib +BuildRequires: libappstream-glib +BuildRequires: make +BuildRequires: ocaml >= 4.04.0 +BuildRequires: ocaml-dune BuildRequires: ocaml-lablgtk-devel +BuildRequires: ocaml-menhir BuildRequires: ocaml-num-devel -BuildRequires: ocaml-ocamlgraph-devel -BuildRequires: ocaml-ocplib-simplex-devel +BuildRequires: ocaml-ocplib-simplex-devel >= 0.4 +BuildRequires: ocaml-psmt2-frontend-devel >= 0.2 BuildRequires: ocaml-zarith-devel BuildRequires: ocaml-zip-devel +Requires: ocaml-alt-ergo-parsers%{?_isa} = %{version}-%{release} + +%global _desc %{expand:Alt-Ergo is an automated theorem prover implemented in OCaml. It is based on +CC(X) - a congruence closure algorithm parameterized by an equational theory +X. This algorithm is reminiscent of the Shostak algorithm. Currently CC(X) +is instantiated by the theory of linear arithmetics. Alt-Ergo also contains a +home made SAT-solver and an instantiation mechanism by which it fully supports +quantifiers.} + %description -Alt-Ergo is an automated theorem prover implemented in OCaml. It is -based on CC(X) - a congruence closure algorithm parameterized by an -equational theory X. This algorithm is reminiscent of the Shostak -algorithm. Currently CC(X) is instantiated by the theory of linear -arithmetics. Alt-Ergo also contains a home made SAT-solver and an -instantiation mechanism by which it fully supports quantifiers. +%_desc %package gui -Summary: Graphical front end for alt-ergo +Summary: Graphical front end for Alt-Ergo +License: CECILL-C Requires: %{name}%{?_isa} = %{version}-%{release} Requires: gtksourceview2 Requires: hicolor-icon-theme -Requires(post): coreutils -Requires(postun): coreutils - %description gui -A graphical front end for the alt-ergo theorem prover. +%_desc + +This package contains a graphical front end for the Alt-Ergo theorem prover. + +%package -n ocaml-alt-ergo-parsers +Summary: Parser library used by the Alt-Ergo SMT solver +License: CECILL-C +Requires: ocaml-alt-ergo-lib%{?_isa} = %{version}-%{release} + +%description -n ocaml-alt-ergo-parsers +%_desc + +This package contains the parser library used by the Alt-Ergo SMT solver. + +%package -n ocaml-alt-ergo-parsers-devel +Summary: Development files for ocaml-alt-ergo-parsers +License: CECILL-C +Requires: ocaml-alt-ergo-parsers%{?_isa} = %{version}-%{release} +Requires: ocaml-alt-ergo-lib-devel%{?_isa} = %{version}-%{release} +Requires: ocaml-psmt2-frontend-devel%{?_isa} +Requires: ocaml-zip-devel%{?_isa} + +%description -n ocaml-alt-ergo-parsers-devel +%_desc + +This package contains development files needed to build applications that use +the Alt-Ergo parser library. + +%package -n ocaml-alt-ergo-lib +Summary: Automated theorem prover library +License: CECILL-C + +%description -n ocaml-alt-ergo-lib +%_desc + +This package is the core of Alt-Ergo as an OCaml library. + +%package -n ocaml-alt-ergo-lib-devel +Summary: Development files for ocaml-alt-ergo-lib +License: CECILL-C +Requires: ocaml-alt-ergo-lib%{?_isa} = %{version}-%{release} +Requires: ocaml-num-devel%{?_isa} +Requires: ocaml-ocplib-simplex-devel%{?_isa} +Requires: ocaml-zarith-devel%{?_isa} + +%description -n ocaml-alt-ergo-lib-devel +%_desc + +This package contains development files needed to build applications that use +the Alt-Ergo library. %prep -%setup -q -%setup -q -T -D -a 1 +%autosetup -n %{name}-%{minorver}.0-free -N -a 2 -%patch1 -p1 - -cp -p %{SOURCE2} . - -# Fix encoding -iconv -f ISO-8859-1 -t UTF-8 -o LICENSE.utf8 LICENSE -touch -r LICENSE LICENSE.utf8 -mv -f LICENSE.utf8 LICENSE - -# Use Fedora LDFLAGS -sed -i "s|^OFLAGS =.*|& -g|" Makefile.users -for arg in $RPM_LD_FLAGS; do - sed -i "s|^OFLAGS =.*-g|& -ccopt $arg|" Makefile.users -done - -%build -%configure - -%if ! %{opt} -%global opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLLEX=ocamllex -%else -%global opt_option OCAMLBEST=opt OCAMLOPT=ocamlopt.opt +%if 0%{?patchrel} > 0 +# See above. Replace the minor release sources with the patch release sources. +rm -rf sources +tar xf %{SOURCE1} %endif -make %{opt_option} -make %{opt_option} gui +%autopatch -p1 + +%conf +cd sources +cp -p %{SOURCE3} com.ocamlpro.%{name}.desktop + +# Unzip an example +cd examples/AB-Why3-plugin +unzip p4_34.why.zip +rm p4_34.why.zip +cd - + +%ifnarch %{ocaml_native_compiler} +# Do not require native plugins +sed -i '/cmxs/d' plugins/{AB-Why3,fm-simplex}/dune +%endif + +# This is not an autoconf-generated script. Do NOT use %%configure. +./configure --prefix=%{_prefix} --libdir=%{ocamldir} --sharedir=%{ocamldir} + +%build +cd sources +%make_build %install -mkdir -p %{buildroot}%{_bindir} -make %{opt_option} DESTDIR=%{buildroot} install install-gui +cd sources +%make_install -# Move the gtksourceview file to the right place -mv %{buildroot}%{_datadir}/%{name}/gtksourceview-2.0 %{buildroot}%{_datadir} -rmdir %{buildroot}%{_datadir}/%{name} +# We do not want the ml files +find %{buildroot}%{ocamldir} -name \*.ml -delete + +# We install the documentation with the doc macro +rm -fr %{buildroot}%{_prefix}/doc + +# Install the man page +mkdir -p %{buildroot}%{_mandir}/man1 +cp -p doc/alt-ergo.1 %{buildroot}%{_mandir}/man1 + +# The install target in the Makefile puts these in the wrong place +mv %{buildroot}%{_datadir}/alt-ergo/{plugins,preludes} \ + %{buildroot}%{ocamldir}/alt-ergo +rmdir %{buildroot}%{_datadir}/alt-ergo + +# Install the gtksourceview file +mkdir -p %{buildroot}%{_datadir}/gtksourceview-2.0/language-specs +cp -p doc/gtk-lang/alt-ergo.lang \ + %{buildroot}%{_datadir}/gtksourceview-2.0/language-specs # Install the desktop file mkdir -p %{buildroot}%{_datadir}/applications -desktop-file-install --dir %{buildroot}%{_datadir}/applications %{name}.desktop +desktop-file-install --dir %{buildroot}%{_datadir}/applications \ + com.ocamlpro.%{name}.desktop # Install the AppData file -mkdir -p %{buildroot}%{_datadir}/appdata -install -pm 644 %{SOURCE3} %{buildroot}%{_datadir}/appdata +mkdir -p %{buildroot}%{_metainfodir} +install -pm 644 %{SOURCE4} \ + %{buildroot}%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml +appstream-util validate-relax --nonet \ + %{buildroot}%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml # Install the icons +cd - mkdir -p %{buildroot}%{_datadir}/icons cp -a icons %{buildroot}%{_datadir}/icons/hicolor +# Put something interesting into the META files +cat > %{buildroot}%{ocamldir}/alt-ergo/META << EOF +version = "%{version}" +description = "Automated theorem prover including linear arithmetic" +requires = "" +EOF +rm %{buildroot}%{ocamldir}/{alt-ergo-free,altgr-ergo}/META +ln %{buildroot}%{ocamldir}/alt-ergo/META \ + %{buildroot}%{ocamldir}/alt-ergo-free/META +ln %{buildroot}%{ocamldir}/alt-ergo/META \ + %{buildroot}%{ocamldir}/altgr-ergo/META + %check -# Test alt-ergo on the examples. -%define altergo %{buildroot}%{_bindir}/alt-ergo -cd examples/valid -for fil in *.why; do - if ! %{altergo} $fil | grep -Fq Valid; then - echo $fil was not found valid - exit 1 - fi -done -cd ../invalid -for fil in *.why; do - if %{altergo} $fil | grep -Fq Valid; then - echo $fil was erroneously found valid - exit 1 - fi -done +cd sources +%dune_check %files -%doc README.md CHANGES examples -%license COPYING.md LICENSE +%doc README.md sources/CHANGES sources/examples publications/*.pdf %{_bindir}/%{name} %{_mandir}/man1/alt-ergo.1.* +%{ocamldir}/%{name}/ +%{ocamldir}/%{name}-free/ %files gui %{_bindir}/altgr-ergo -%{_datadir}/appdata/%{name}.appdata.xml -%{_datadir}/applications/%{name}.desktop +%{_datadir}/applications/com.ocamlpro.%{name}.desktop %{_datadir}/gtksourceview-2.0/language-specs/%{name}.lang %{_datadir}/icons/hicolor/*/apps/%{name}.png +%{ocamldir}/altgr-ergo/ +%{_metainfodir}/com.ocamlpro.%{name}.metainfo.xml + +%files -n ocaml-%{name}-parsers +%dir %{ocamldir}/%{name}-parsers/ +%{ocamldir}/%{name}-parsers/META +%{ocamldir}/%{name}-parsers/*.cma +%{ocamldir}/%{name}-parsers/*.cmi +%ifarch %{ocaml_native_compiler} +%{ocamldir}/%{name}-parsers/*.cmxs +%endif +%{ocamldir}/%{name}-parsers-free/ + +%files -n ocaml-%{name}-parsers-devel +%{ocamldir}/%{name}-parsers/dune-package +%{ocamldir}/%{name}-parsers/opam +%ifarch %{ocaml_native_compiler} +%{ocamldir}/%{name}-parsers/*.a +%{ocamldir}/%{name}-parsers/*.cmx +%{ocamldir}/%{name}-parsers/*.cmxa +%endif +%{ocamldir}/%{name}-parsers/*.mli +%{ocamldir}/%{name}-parsers/*.cmt +%{ocamldir}/%{name}-parsers/*.cmti + +%files -n ocaml-%{name}-lib +%dir %{ocamldir}/%{name}-lib/ +%license LGPL-License.txt LICENSE.md License.OCamlPro +%{ocamldir}/%{name}-lib/META +%{ocamldir}/%{name}-lib/*.cma +%{ocamldir}/%{name}-lib/*.cmi +%ifarch %{ocaml_native_compiler} +%{ocamldir}/%{name}-lib/*.cmxs +%endif +%{ocamldir}/%{name}-lib-free/ + +%files -n ocaml-%{name}-lib-devel +%{ocamldir}/%{name}-lib/dune-package +%{ocamldir}/%{name}-lib/opam +%{ocamldir}/%{name}-lib/frontend/ +%{ocamldir}/%{name}-lib/reasoners/ +%{ocamldir}/%{name}-lib/structures/ +%{ocamldir}/%{name}-lib/util/ +%ifarch %{ocaml_native_compiler} +%{ocamldir}/%{name}-lib/*.a +%{ocamldir}/%{name}-lib/*.cmx +%{ocamldir}/%{name}-lib/*.cmxa +%endif +%{ocamldir}/%{name}-lib/*.cmt +%{ocamldir}/%{name}-lib/*.cmti %changelog +* Fri Jan 16 2026 Fedora Release Engineering - 2.3.3-30 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild + +* Tue Oct 14 2025 Richard W.M. Jones - 2.3.3-29 +- OCaml 5.4.0 rebuild + +* Tue Sep 16 2025 Jerry James - 2.3.3-28 +- Rebuild for ocaml-menhir 20250912 + +* Fri Sep 05 2025 Jerry James - 2.3.3-27 +- Rebuild for ocaml-menhir 20250903 + +* Wed Jul 23 2025 Fedora Release Engineering - 2.3.3-26 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild + +* Fri Jul 11 2025 Jerry James - 2.3.3-25 +- Rebuild to fix OCaml dependencies + +* Thu Jan 16 2025 Fedora Release Engineering - 2.3.3-24 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild + +* Thu Jan 9 2025 Jerry James - 2.3.3-23 +- OCaml 5.3.0 rebuild for Fedora 42 +- Correct License fields from Apache-2.0 to CECILL-C +- Do configuration steps in %%conf + +* Mon Aug 5 2024 Jerry James - 2.3.3-22 +- Rebuild for ocaml-menhir 20240715 and ocaml-zip 1.12 + +* Wed Jul 17 2024 Fedora Release Engineering - 2.3.3-21 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild + +* Tue Jul 16 2024 Jerry James - 2.3.3-20 +- Rebuild for ocaml-zarith 1.14 + +* Wed Jun 19 2024 Richard W.M. Jones - 2.3.3-19 +- OCaml 5.2.0 ppc64le fix + +* Wed May 29 2024 Richard W.M. Jones - 2.3.3-18 +- OCaml 5.2.0 for Fedora 41 + +* Thu May 23 2024 Jerry James - 2.3.3-17 +- Add patch to fix misplaced inline attributes + +* Fri Feb 2 2024 Jerry James - 2.3.3-17 +- Rebuild for changed ocamlx(Dynlink) hash + +* Mon Jan 22 2024 Fedora Release Engineering - 2.3.3-16 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild + +* Fri Jan 19 2024 Fedora Release Engineering - 2.3.3-15 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild + +* Tue Jan 2 2024 Jerry James - 2.3.3-14 +- Rebuild for ocaml-num and ocaml-menhir 20231231 + +* Mon Dec 18 2023 Richard W.M. Jones - 2.3.3-13 +- OCaml 5.1.1 + s390x code gen fix for Fedora 40 + +* Tue Dec 12 2023 Richard W.M. Jones - 2.3.3-12 +- OCaml 5.1.1 rebuild for Fedora 40 + +* Thu Oct 05 2023 Richard W.M. Jones - 2.3.3-11 +- OCaml 5.1 rebuild for Fedora 40 + +* Thu Jul 27 2023 Jerry James - 2.3.3-10 +- Rebuild for ocaml-zarith 1.13 + +* Wed Jul 19 2023 Fedora Release Engineering - 2.3.3-9 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild + +* Tue Jul 18 2023 Jerry James - 2.3.3-8 +- Validate appdata with appstream-util + +* Wed Jul 12 2023 Richard W.M. Jones - 2.3.3-8 +- OCaml 5.0 rebuild for Fedora 39 + +* Mon Jul 10 2023 Jerry James - 2.3.3-7 +- OCaml 5.0.0 rebuild + +* Fri Mar 24 2023 Jerry James - 2.3.3-6 +- Dune 3.7.0 changed the install location of mli files + +* Tue Jan 24 2023 Richard W.M. Jones - 2.3.3-5 +- Rebuild OCaml packages for F38 + +* Wed Jan 18 2023 Fedora Release Engineering - 2.3.3-4 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild + +* Thu Aug 11 2022 Jerry James - 2.3.3-3 +- Convert License tag to SPDX +- Note that the AB plugin has a different license + +* Wed Jul 20 2022 Fedora Release Engineering - 2.3.3-3 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild + +* Tue Jul 5 2022 Jerry James - 2.3.3-2 +- Patch out uses of the dune external-lib-deps command +- Patch out references to the seq forward compatibility module +- Use new OCaml macros + +* Mon Jun 20 2022 Jerry James - 2.3.3-1 +- Version 2.3.3 +- Add -menhir patch to fix FTBFS +- Add -stdlib-shims patch since Fedora does not need stdlib-shims + +* Sun Jun 19 2022 Richard W.M. Jones - 2.3.0-5 +- OCaml 4.14.0 rebuild + +* Mon Feb 28 2022 Jerry James - 2.3.0-4 +- Switch to the correct tarball +- Drop unneeded ocaml-findlib BR +- Add dependency on ocaml-alt-ergo-parsers from ocaml-alt-ergo-parsers-devel + +* Fri Feb 04 2022 Richard W.M. Jones - 2.3.0-3 +- OCaml 4.13.1 rebuild to remove package notes + +* Wed Jan 19 2022 Fedora Release Engineering - 2.3.0-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild + +* Mon Dec 27 2021 Jerry James - 2.3.0-1 +- Version 2.3.0 +- New ocaml-alt-ergo-lib and ocaml-alt-ergo-parsers subpackages + +* Tue Oct 05 2021 Richard W.M. Jones - 2.2.0-14 +- OCaml 4.13.1 build + +* Thu Jul 29 2021 Jerry James - 2.2.0-13 +- Rebuild for changed ocamlx(Dynlink) + +* Wed Jul 21 2021 Fedora Release Engineering - 2.2.0-12 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild + +* Mon Jul 19 2021 Jerry James - 2.2.0-11 +- Move META to the main package + +* Tue Jun 22 2021 Jerry James - 2.2.0-11 +- Rebuild for ocaml-lablgtk without gnomeui + +* Wed Mar 3 2021 Jerry James - 2.2.0-10 +- Rebuild for ocaml-zarith 1.12 + +* Tue Mar 2 11:26:14 GMT 2021 Richard W.M. Jones - 2.2.0-9 +- OCaml 4.12.0 build + +* Thu Feb 4 2021 Jerry James - 2.2.0-8 +- Updates to the desktop and metainfo files +- Add -pervasives patch + +* Tue Jan 26 2021 Fedora Release Engineering - 2.2.0-7 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild + +* Mon Nov 16 2020 Jerry James - 2.2.0-6 +- Rebuild for ocaml-zarith 1.11 + +* Fri Sep 25 2020 Jerry James - 2.2.0-5 +- Rebuild for ocaml-zarith 1.10 + +* Tue Sep 01 2020 Richard W.M. Jones - 2.2.0-4 +- OCaml 4.11.1 rebuild + +* Fri Aug 21 2020 Richard W.M. Jones - 2.2.0-3 +- OCaml 4.11.0 rebuild + +* Mon Jul 27 2020 Fedora Release Engineering - 2.2.0-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild + +* Fri Jun 19 2020 Jerry James - 2.2.0-1 +- Version 2.2.0 +- Drop upstreamed -newline patch + +* Tue May 05 2020 Richard W.M. Jones - 2.0.0-15 +- OCaml 4.11.0+dev2-2020-04-22 rebuild + +* Wed Apr 22 2020 Richard W.M. Jones - 2.0.0-14 +- OCaml 4.11.0 pre-release attempt 2 + +* Wed Apr 8 2020 Jerry James - 2.0.0-13 +- Filter out Requires for private interfaces we do not Provide + +* Fri Apr 03 2020 Richard W.M. Jones - 2.0.0-12 +- Update all OCaml dependencies for RPM 4.16. + +* Mon Mar 30 2020 Jerry James - 2.0.0-11 +- Rebuild for ocaml-zip 1.10 + +* Tue Mar 24 2020 Jerry James - 2.0.0-10 +- Rebuild for ocaml-menhir 20200211 + +* Wed Feb 26 2020 Richard W.M. Jones - 2.0.0-9 +- OCaml 4.10.0 final. + +* Tue Jan 28 2020 Fedora Release Engineering - 2.0.0-8 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild + +* Sun Jan 19 2020 Richard W.M. Jones - 2.0.0-7 +- OCaml 4.10.0+beta1 rebuild. + +* Fri Dec 06 2019 Richard W.M. Jones - 2.0.0-6 +- OCaml 4.09.0 (final) rebuild. + +* Fri Sep 6 2019 Jerry James - 2.0.0-5 +- Rebuild for ocaml-zarith 1.9 + +* Fri Aug 16 2019 Richard W.M. Jones - 2.0.0-4 +- OCaml 4.08.1 (final) rebuild. + +* Wed Jul 31 2019 Richard W.M. Jones - 2.0.0-3 +- OCaml 4.08.1 (rc2) rebuild. + +* Wed Jul 24 2019 Fedora Release Engineering - 2.0.0-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild + +* Wed Jun 5 2019 Jerry James - 2.0.0-1 +- Update to version 2.0.0 +- Add -newline patch to fix FTBFS +- Add a 256x256 icon + +* Thu Jan 31 2019 Fedora Release Engineering - 1.30-16 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild + +* Thu Jul 12 2018 Fedora Release Engineering - 1.30-15 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild + +* Wed Jul 11 2018 Richard W.M. Jones - 1.30-14 +- OCaml 4.07.0 (final) rebuild. + +* Wed Jun 20 2018 Richard W.M. Jones - 1.30-13 +- OCaml 4.07.0-rc1 rebuild. + * Wed Feb 07 2018 Fedora Release Engineering - 1.30-12 - Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild diff --git a/sources b/sources index 6f0dcae..2e808e5 100644 --- a/sources +++ b/sources @@ -1,2 +1,3 @@ -c7100ebd625fbd7d3e5247dbac689748 alt-ergo-1.30.tar.gz -90052f03870cc94a1ceb8ac3fae77b7b alt-ergo-icons.tar.xz +SHA512 (alt-ergo-free-2.3.0.tar.gz) = e15efc6bbde59065c6ccaf1ef2f8158b8b9be4b00b2c2365e5eeb7d7114be72c47c813fc06880a6278edd7e288f24ef4588c88e0630d9bda9378a3eda3fd07ca +SHA512 (alt-ergo-free-2.3.3.tar.gz) = 0dc056c02c8ffdeb9eeaa127dd204d30a0ee95ffe38aa3f1a608b17019f377ea6520ccfc9cb09b109deac5f19e7e695b7e6ec18db969843312cfb17f3950c9ba +SHA512 (alt-ergo-icons.tar.xz) = cb2e93bab3359f6f198e80e3e68840ed4b25a213b61f388a2de8abc299fd3c89240f64f610290ac89e6005088c484b2718a68ec18063076f73d7871a38ee038f