Compare commits
3 commits
| Author | SHA1 | Date | |
|---|---|---|---|
|
dd89886031 | ||
|
|
3a9e6768d8 | ||
|
|
e15e762331 |
6 changed files with 34 additions and 135 deletions
|
|
@ -1,6 +1,6 @@
|
|||
<?xml version="1.0" encoding="UTF-8"?>
|
||||
<component type="desktop-application">
|
||||
<id>why3.desktop</id>
|
||||
<id>fr.lri.why3.desktop</id>
|
||||
<metadata_license>0BSD</metadata_license>
|
||||
<project_license>LGPL-2.1-only WITH OCaml-LGPL-linking-exception</project_license>
|
||||
<name>Why3</name>
|
||||
|
|
@ -15,27 +15,27 @@
|
|||
TPTP provers, as well as interactive proof assistants.
|
||||
</p>
|
||||
</description>
|
||||
<launchable type="desktop-id">why3.desktop</launchable>
|
||||
<launchable type="desktop-id">fr.lri.why3.desktop</launchable>
|
||||
<screenshots>
|
||||
<screenshot type="default">
|
||||
<image>http://why3.lri.fr/doc/gui-1.png</image>
|
||||
<image>http://why3.lri.fr/doc/_images/gui-1.png</image>
|
||||
<caption>Initial Why3 GUI window</caption>
|
||||
</screenshot>
|
||||
<screenshot>
|
||||
<image>http://why3.lri.fr/doc/gui-2.png</image>
|
||||
<image>The Why3 GUI with goal G1 selected</image>
|
||||
<image>http://why3.lri.fr/doc/_images/gui-2.png</image>
|
||||
<caption>The Why3 GUI with goal G1 selected</caption>
|
||||
</screenshot>
|
||||
<screenshot>
|
||||
<image>http://why3.lri.fr/doc/gui-3.png</image>
|
||||
<image>The Why3 GUI after running Alt-Ergo on each goal</image>
|
||||
<image>http://why3.lri.fr/doc/_images/gui-3.png</image>
|
||||
<caption>The Why3 GUI after running Alt-Ergo on each goal</caption>
|
||||
</screenshot>
|
||||
<screenshot>
|
||||
<image>http://why3.lri.fr/doc/gui-4.png</image>
|
||||
<image>The Why3 GUI after splitting goal G2</image>
|
||||
<image>http://why3.lri.fr/doc/_images/gui-4.png</image>
|
||||
<caption>The Why3 GUI after splitting goal G2</caption>
|
||||
</screenshot>
|
||||
<screenshot>
|
||||
<image>http://why3.lri.fr/doc/gui-5.png</image>
|
||||
<image>File reloaded after modifying goal G2</image>
|
||||
<image>http://why3.lri.fr/doc/_images/gui-5.png</image>
|
||||
<caption>File reloaded after modifying goal G2</caption>
|
||||
</screenshot>
|
||||
</screenshots>
|
||||
<update_contact>loganjerry@gmail.com</update_contact>
|
||||
2
sources
2
sources
|
|
@ -1,2 +1,2 @@
|
|||
SHA512 (why3-man.tar.xz) = 8355776ac8a67a56ae7354f8fd40dc5d2057022d1035090a3e38e139fbfe3c258fe3ccbed6e333cb005e66c7b4cdbbf6580e3420170fd08384cc9b36ce5ec2a1
|
||||
SHA512 (why3-1.3.3.tar.gz) = a2dc95691cea29bbd20843a05add3985f777085086b654b53566ecdb752ba892366da703e232c85d5e0237d0e59564527aed55f6ccae9118d49e5f2cf93a53ce
|
||||
SHA512 (why3-1.4.0.tar.gz) = b492f08a3c7073782b143a4849c47766b12045ad53c56aa8d251fd5b6bc1863ddebe260c99b3ddb27c4e1e1e9ab986c8b02286ec24f4c30f99f81f5f13fdc90a
|
||||
|
|
|
|||
|
|
@ -1,99 +0,0 @@
|
|||
--- configure.in.orig 2020-09-11 08:06:19.000000000 -0600
|
||||
+++ configure.in 2021-02-06 20:18:51.197299198 -0700
|
||||
@@ -869,6 +869,9 @@ if test "$enable_coq_support" = yes; the
|
||||
8.12*)
|
||||
coq_compat_version="COQ812"
|
||||
;;
|
||||
+ 8.13*)
|
||||
+ coq_compat_version="COQ813"
|
||||
+ ;;
|
||||
*)
|
||||
enable_coq_support=no
|
||||
AC_MSG_WARN(You need Coq 8.6 or later; Coq discarded)
|
||||
--- configure.orig 2020-09-11 08:06:19.000000000 -0600
|
||||
+++ configure 2021-02-06 20:19:13.736250432 -0700
|
||||
@@ -5365,6 +5365,9 @@ $as_echo "$COQVERSION" >&6; }
|
||||
8.12*)
|
||||
coq_compat_version="COQ812"
|
||||
;;
|
||||
+ 8.13*)
|
||||
+ coq_compat_version="COQ813"
|
||||
+ ;;
|
||||
*)
|
||||
enable_coq_support=no
|
||||
{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: You need Coq 8.6 or later; Coq discarded" >&5
|
||||
--- lib/coq/ieee_float/GenericFloat.v.orig 2020-09-11 08:06:19.000000000 -0600
|
||||
+++ lib/coq/ieee_float/GenericFloat.v 2021-02-06 20:19:40.687192153 -0700
|
||||
@@ -3726,7 +3726,8 @@ Proof.
|
||||
assert (- pow2sb <= pow2sb <= pow2sb)%Z.
|
||||
split; auto with zarith.
|
||||
assert (0 < pow2sb)%Z.
|
||||
- apply (Z.pow_pos_nonneg 2 sb); auto with zarith.
|
||||
+ apply (Z.pow_pos_nonneg 2 sb).
|
||||
+ easy.
|
||||
apply Z.lt_le_incl, Hsb'.
|
||||
auto with zarith.
|
||||
|
||||
--- lib/coq/set/FsetInt.v.orig 2020-09-11 08:06:19.000000000 -0600
|
||||
+++ lib/coq/set/FsetInt.v 2021-02-06 20:21:15.476987120 -0700
|
||||
@@ -166,15 +166,13 @@ induction len; eauto.
|
||||
intros. simpl. rewrite IHlen. reflexivity.
|
||||
Qed.
|
||||
|
||||
-(* Why3 goal *)
|
||||
-Definition interval :
|
||||
- Numbers.BinNums.Z -> Numbers.BinNums.Z -> set.Fset.fset Numbers.BinNums.Z.
|
||||
+Lemma interval_proof :
|
||||
+ forall l r : int, exists s : list int,
|
||||
+ List.NoDup s /\
|
||||
+ forall e : int, List.In e s <->
|
||||
+ (if Z_le_dec l e then if Z_lt_dec e r then true else false else false) = true.
|
||||
Proof.
|
||||
intros l r.
|
||||
-exists (fun x => if Z_le_dec l x then
|
||||
- if Z_lt_dec x r then true
|
||||
- else false
|
||||
- else false).
|
||||
destruct (Z_le_dec l r).
|
||||
+ exists (seqZ l (Z.to_nat (r - l))%Z).
|
||||
split.
|
||||
@@ -185,8 +183,8 @@ destruct (Z_le_dec l r).
|
||||
destruct Z_le_dec.
|
||||
* destruct Z_lt_dec. split; intros; [reflexivity|].
|
||||
intuition.
|
||||
- intuition. inversion H.
|
||||
- * intuition. inversion H.
|
||||
+ intuition ; try inversion H.
|
||||
+ * intuition ; try inversion H.
|
||||
+ exists List.nil.
|
||||
split.
|
||||
- constructor.
|
||||
@@ -195,6 +193,18 @@ destruct (Z_le_dec l r).
|
||||
omega.
|
||||
inversion H.
|
||||
inversion H.
|
||||
+Qed.
|
||||
+
|
||||
+(* Why3 goal *)
|
||||
+Definition interval :
|
||||
+ Numbers.BinNums.Z -> Numbers.BinNums.Z -> set.Fset.fset Numbers.BinNums.Z.
|
||||
+Proof.
|
||||
+intros l r.
|
||||
+exists (fun x =>
|
||||
+ if Z_le_dec l x then
|
||||
+ if Z_lt_dec x r then true else false
|
||||
+ else false).
|
||||
+apply interval_proof.
|
||||
Defined.
|
||||
|
||||
(* Why3 goal *)
|
||||
--- share/provers-detection-data.conf.orig 2020-09-11 08:06:19.000000000 -0600
|
||||
+++ share/provers-detection-data.conf 2021-02-06 20:21:48.348916001 -0700
|
||||
@@ -751,6 +751,7 @@ support_library = "%l/coq/version"
|
||||
exec = "coqtop"
|
||||
version_switch = "-v"
|
||||
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
|
||||
+version_ok = "^8\.13\.[0-9]+$"
|
||||
version_ok = "^8\.12\.[0-9]+$"
|
||||
version_ok = "^8\.11\.[0-9]+$"
|
||||
version_ok = "^8\.10\.[0-9]+$"
|
||||
|
|
@ -1,10 +0,0 @@
|
|||
--- doc/conf.py.orig 2020-09-11 08:06:19.000000000 -0600
|
||||
+++ doc/conf.py 2020-12-23 08:29:46.914254118 -0700
|
||||
@@ -50,6 +50,7 @@ master_doc = 'index'
|
||||
project = 'Why3'
|
||||
copyright = '2020, The Why3 Development Team'
|
||||
author = 'The Why3 Development Team'
|
||||
+bibtex_bibfiles = ['manual.bib']
|
||||
|
||||
# The version info for the project you're documenting, acts as replacement for
|
||||
# |version| and |release|, also used in various other places throughout the
|
||||
36
why3.spec
36
why3.spec
|
|
@ -8,35 +8,30 @@
|
|||
%endif
|
||||
|
||||
Name: why3
|
||||
Version: 1.3.3
|
||||
Release: 6%{?dist}
|
||||
Version: 1.4.0
|
||||
Release: 1%{?dist}
|
||||
Summary: Software verification platform
|
||||
|
||||
# See LICENSE for the terms of the exception
|
||||
License: LGPLv2 with exceptions
|
||||
URL: http://why3.lri.fr/
|
||||
Source0: https://gforge.inria.fr/frs/download.php/file/38367/%{name}-%{version}.tar.gz
|
||||
Source0: https://gforge.inria.fr/frs/download.php/file/38425/%{name}-%{version}.tar.gz
|
||||
# Man pages written by Jerry James using text found in the sources. Hence,
|
||||
# the copyright and license are the same as for the upstream sources.
|
||||
Source1: %{name}-man.tar.xz
|
||||
# Desktop file written by Jerry James
|
||||
Source2: %{name}.desktop
|
||||
Source2: fr.lri.%{name}.desktop
|
||||
# AppData file written by Jerry James
|
||||
Source3: %{name}.metainfo.xml
|
||||
# Adapt to sphinxcontrib-bibtex 2.x
|
||||
Patch0: %{name}-sphinxcontrib-bibtex.patch
|
||||
# Permit use of coq 8.13.0
|
||||
# https://gitlab.inria.fr/why3/why3/-/commit/31b5bf527804793c10f26acd2a14045be71d256c
|
||||
Patch1: %{name}-coq8.13.patch
|
||||
Source3: fr.lri.%{name}.metainfo.xml
|
||||
|
||||
# https://bugzilla.redhat.com/show_bug.cgi?id=1874879
|
||||
ExcludeArch: s390x
|
||||
|
||||
BuildRequires: appstream
|
||||
BuildRequires: coq
|
||||
BuildRequires: emacs-proofgeneral
|
||||
BuildRequires: flocq
|
||||
BuildRequires: latexmk
|
||||
BuildRequires: libappstream-glib
|
||||
BuildRequires: make
|
||||
BuildRequires: ocaml
|
||||
BuildRequires: ocaml-camlp5-devel
|
||||
|
|
@ -244,7 +239,8 @@ cp -p share/images/src/logo-kim.svg \
|
|||
# Install the AppStream metadata
|
||||
mkdir -p %{buildroot}%{_metainfodir}
|
||||
cp -p %{SOURCE3} %{buildroot}%{_metainfodir}
|
||||
appstream-util validate-relax --nonet %{buildroot}%{_metainfodir}/%{name}.metainfo.xml
|
||||
appstreamcli validate --no-net \
|
||||
%{buildroot}%{_metainfodir}/fr.lri.%{name}.metainfo.xml
|
||||
|
||||
# Move the vim file to the right place
|
||||
mkdir -p %{buildroot}%{_datadir}/vim/vimfiles
|
||||
|
|
@ -277,7 +273,7 @@ chmod 0755 %{buildroot}%{_bindir}/* \
|
|||
%license LICENSE
|
||||
%{_bindir}/%{name}
|
||||
%{_datadir}/%{name}/
|
||||
%{_datadir}/applications/%{name}.desktop
|
||||
%{_datadir}/applications/fr.lri.%{name}.desktop
|
||||
%{_datadir}/bash-completion/completions/why3
|
||||
%{_datadir}/gtksourceview-3.0/language-specs/%{name}.lang
|
||||
%{_datadir}/gtksourceview-3.0/language-specs/%{name}c.lang
|
||||
|
|
@ -289,7 +285,7 @@ chmod 0755 %{buildroot}%{_bindir}/* \
|
|||
%{_texmf}/tex/latex/why3/
|
||||
%{_libdir}/%{name}/
|
||||
%{_mandir}/man1/%{name}*
|
||||
%{_metainfodir}/%{name}.metainfo.xml
|
||||
%{_metainfodir}/fr.lri.%{name}.metainfo.xml
|
||||
|
||||
%files -n ocaml-%{name}
|
||||
%dir %{_libdir}/ocaml/%{name}/
|
||||
|
|
@ -307,6 +303,7 @@ chmod 0755 %{buildroot}%{_bindir}/* \
|
|||
%else
|
||||
%{_libdir}/ocaml/%{name}/*.cma
|
||||
%endif
|
||||
%{_libdir}/ocaml/%{name}/*.cmt
|
||||
|
||||
%files examples
|
||||
%doc examples
|
||||
|
|
@ -326,6 +323,17 @@ chmod 0755 %{buildroot}%{_bindir}/* \
|
|||
%files all
|
||||
|
||||
%changelog
|
||||
* Wed Jul 14 2021 Jerry James <loganjerry@gmail.com> - 1.4.0-1
|
||||
- Version 1.4.0
|
||||
- Drop all patches
|
||||
- Validate with appstreamcli instead of appstream-util
|
||||
|
||||
* Tue Jun 8 2021 Jerry James <loganjerry@gmail.com> - 1.3.3-8
|
||||
- Rebuild for ocaml-menhir 20210419
|
||||
|
||||
* Wed Mar 3 2021 Jerry James <loganjerry@gmail.com> - 1.3.3-7
|
||||
- Rebuild for coq 8.13.1 and ocaml-zarith 1.12
|
||||
|
||||
* Sat Feb 20 2021 Jerry James <loganjerry@gmail.com> - 1.3.3-6
|
||||
- Rebuild for coq 8.13.0
|
||||
- Update metainfo and install in metainfodir
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue