diff --git a/.gitignore b/.gitignore index 7da3b50..e139737 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,4 @@ /alt-ergo-icons.tar.xz -/alt-ergo-*.tar.gz +/alt-ergo-0.99.1.tar.gz +/alt-ergo-1.01.tar.gz +/alt-ergo-1.30.tar.gz diff --git a/README.md b/README.md deleted file mode 100644 index fa65fbb..0000000 --- a/README.md +++ /dev/null @@ -1,9 +0,0 @@ -# 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-dune3.patch b/alt-ergo-dune3.patch deleted file mode 100644 index cb875a4..0000000 --- a/alt-ergo-dune3.patch +++ /dev/null @@ -1,29 +0,0 @@ ---- 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 deleted file mode 100644 index b3be679..0000000 --- a/alt-ergo-forward-compat.patch +++ /dev/null @@ -1,64 +0,0 @@ ---- 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 deleted file mode 100644 index ccb8356..0000000 --- a/alt-ergo-inline-error.patch +++ /dev/null @@ -1,26 +0,0 @@ -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 deleted file mode 100644 index 4ab3e45..0000000 --- a/alt-ergo-menhir.patch +++ /dev/null @@ -1,18 +0,0 @@ ---- 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 deleted file mode 100644 index bd72f54..0000000 --- a/alt-ergo-pervasives.patch +++ /dev/null @@ -1,172 +0,0 @@ ---- 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 deleted file mode 100644 index caa9af7..0000000 --- a/alt-ergo-psmt2-frontend.patch +++ /dev/null @@ -1,12 +0,0 @@ ---- 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.metainfo.xml b/alt-ergo.appdata.xml similarity index 62% rename from alt-ergo.metainfo.xml rename to alt-ergo.appdata.xml index cff34da..145c9a1 100644 --- a/alt-ergo.metainfo.xml +++ b/alt-ergo.appdata.xml @@ -1,6 +1,6 @@ - - com.ocamlpro.alt-ergo + + alt-ergo.desktop CC0-1.0 CECILL-C Alt-Ergo @@ -17,19 +17,13 @@ by which it fully supports quantifiers.

- com.ocamlpro.alt-ergo.desktop - https://jjames.fedorapeople.org/alt-ergo/altgr-ergo-screenshot.png + http://jjames.fedorapeople.org/alt-ergo/altgr-ergo-screenshot.png Basic Alt-Ergo usage - alt-ergo-maintainers@fedoraproject.org - https://alt-ergo.ocamlpro.com/ + loganjerry@gmail.com + http://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 3adb6d8..45d410d 100644 --- a/alt-ergo.spec +++ b/alt-ergo.spec @@ -1,555 +1,144 @@ -# 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. -# 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 +%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0) +%if !%{opt} +%global debug_package %{nil} +%endif Name: alt-ergo -Version: %{minorver}.%{patchrel} -Release: 30%{?dist} +Version: 1.30 +Release: 1%{?dist} Summary: Automated theorem prover including linear arithmetic +License: CeCILL-C -# 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 +URL: http://alt-ergo.ocamlpro.com/ +Source0: http://alt-ergo.ocamlpro.com/http/%{name}-%{version}/%{name}-%{version}.tar.gz # Created with gimp from official upstream icon -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 +Source1: %{name}-icons.tar.xz +Source2: %{name}.desktop +Source3: %{name}.appdata.xml BuildRequires: desktop-file-utils BuildRequires: gtksourceview2-devel -BuildRequires: libappstream-glib -BuildRequires: make -BuildRequires: ocaml >= 4.04.0 -BuildRequires: ocaml-dune +BuildRequires: ocaml +BuildRequires: ocaml-findlib BuildRequires: ocaml-lablgtk-devel -BuildRequires: ocaml-menhir -BuildRequires: ocaml-num-devel -BuildRequires: ocaml-ocplib-simplex-devel >= 0.4 -BuildRequires: ocaml-psmt2-frontend-devel >= 0.2 +BuildRequires: ocaml-ocamlgraph-devel +BuildRequires: ocaml-ocplib-simplex-devel 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 -%_desc +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. %package gui -Summary: Graphical front end for Alt-Ergo -License: CECILL-C +Summary: Graphical front end for alt-ergo Requires: %{name}%{?_isa} = %{version}-%{release} Requires: gtksourceview2 Requires: hicolor-icon-theme +Requires(post): coreutils +Requires(postun): coreutils + %description gui -%_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. +A graphical front end for the alt-ergo theorem prover. %prep -%autosetup -n %{name}-%{minorver}.0-free -N -a 2 +%setup -q +%setup -q -T -D -a 1 -%if 0%{?patchrel} > 0 -# See above. Replace the minor release sources with the patch release sources. -rm -rf sources -tar xf %{SOURCE1} -%endif +cp -p %{SOURCE2} . -%autopatch -p1 +# Fix encoding +iconv -f ISO-8859-1 -t UTF-8 -o LICENSE.utf8 LICENSE +touch -r LICENSE LICENSE.utf8 +mv -f LICENSE.utf8 LICENSE -%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} +# 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 -cd sources -%make_build +%configure + +%if ! %{opt} +%global opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLLEX=ocamllex +%else +%global opt_option OCAMLBEST=opt OCAMLOPT=ocamlopt.opt +%endif + +make %{opt_option} +make %{opt_option} gui %install -cd sources -%make_install +mkdir -p %{buildroot}%{_bindir} +make %{opt_option} DESTDIR=%{buildroot} install install-gui -# 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 +# Move the gtksourceview file to the right place +mv %{buildroot}%{_datadir}/%{name}/gtksourceview-2.0 %{buildroot}%{_datadir} +rmdir %{buildroot}%{_datadir}/%{name} # Install the desktop file mkdir -p %{buildroot}%{_datadir}/applications -desktop-file-install --dir %{buildroot}%{_datadir}/applications \ - com.ocamlpro.%{name}.desktop +desktop-file-install --dir %{buildroot}%{_datadir}/applications %{name}.desktop # Install the AppData file -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 +mkdir -p %{buildroot}%{_datadir}/appdata +install -pm 644 %{SOURCE3} %{buildroot}%{_datadir}/appdata # 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 +%post gui +touch --no-create %{_datadir}/icons/hicolor &>/dev/null +gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || : + +%postun gui +touch --no-create %{_datadir}/icons/hicolor &>/dev/null +gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || : %check -cd sources -%dune_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 %files -%doc README.md sources/CHANGES sources/examples publications/*.pdf +%doc README.md CHANGES examples +%license COPYING.md LICENSE %{_bindir}/%{name} %{_mandir}/man1/alt-ergo.1.* -%{ocamldir}/%{name}/ -%{ocamldir}/%{name}-free/ %files gui %{_bindir}/altgr-ergo -%{_datadir}/applications/com.ocamlpro.%{name}.desktop +%{_datadir}/appdata/%{name}.appdata.xml +%{_datadir}/applications/%{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 - -* Sun Jan 07 2018 Igor Gnatenko - 1.30-11 -- Remove obsolete scriptlets - -* Wed Nov 08 2017 Richard W.M. Jones - 1.30-10 -- OCaml 4.06.0 rebuild. - -* Mon Aug 07 2017 Richard W.M. Jones - 1.30-9 -- OCaml 4.05.0 rebuild. - -* Wed Aug 02 2017 Fedora Release Engineering - 1.30-8 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild - -* Wed Jul 26 2017 Fedora Release Engineering - 1.30-7 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild - -* Mon Jun 26 2017 Richard W.M. Jones - 1.30-6 -- OCaml 4.04.2 rebuild. - -* Fri May 12 2017 Richard W.M. Jones - 1.30-5 -- Bump release and rebuild. - -* Fri May 12 2017 Richard W.M. Jones - 1.30-4 -- Bump release and rebuild. - -* Fri May 12 2017 Richard W.M. Jones - 1.30-3 -- OCaml 4.04.1 rebuild. - -* Fri Feb 10 2017 Fedora Release Engineering - 1.30-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild - * Mon Nov 28 2016 Jerry James - 1.30-1 - Update to version 1.30 diff --git a/sources b/sources index 2e808e5..6f0dcae 100644 --- a/sources +++ b/sources @@ -1,3 +1,2 @@ -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 +c7100ebd625fbd7d3e5247dbac689748 alt-ergo-1.30.tar.gz +90052f03870cc94a1ceb8ac3fae77b7b alt-ergo-icons.tar.xz