rpm/coq
SHA256
1
0
Fork 0
forked from pool/coq
Code Pull Requests Activity

- Update to version 8.20.0. The most impactful changes are:

Browse Source 
* A mechanism to add user-defined rewrite rules to Coq's reduction
    mechanisms; see chapter "User-defined rewrite rules".
  * Support for primitive strings in terms.
  * Reduction of the bytecode segment size, which in turn means
    that `.vo` files might now be considerably smaller.
- Notable breaking changes:
  * Syntactic global references passed through the `using` clauses
    of `auto`-like tactics are now handled as plain references
    rather than interpreted terms. In particular, their typeclass
    arguments will not be inferred. In general, the previous
    behaviour can be emulated by replacing `auto using foo` with
    `pose proof foo; auto`.
  * Argument order for the Ltac2 combinators `List.fold_left2` and
    `List.fold_right2` changed to be the same as in OCaml.
  * Importing a module containing a mutable Ltac2 definition does
    not undo its mutations. Replace `Ltac2 mutable foo :=
    some_expr.` with `Ltac2 mutable foo := some_expr. Ltac2 Set foo
    := some_expr.` to recover the previous behaviour.
  * Some renaming in the standard library. Deprecations are
    provided for a smooth transition.
- For more details, see the change log in coq-doc.

OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=67
This commit is contained in:
Aaron Puchert 2024-09-07 15:01:23 +00:00 committed by Git OBS Bridge
commit 9c22c89df3
15 changed files with 1156 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
.gitattributes vendored Normal file
View File

@ -0,0 +1,23 @@
## Default LFS
*.7z filter=lfs diff=lfs merge=lfs -text
*.bsp filter=lfs diff=lfs merge=lfs -text
*.bz2 filter=lfs diff=lfs merge=lfs -text
*.gem filter=lfs diff=lfs merge=lfs -text
*.gz filter=lfs diff=lfs merge=lfs -text
*.jar filter=lfs diff=lfs merge=lfs -text
*.lz filter=lfs diff=lfs merge=lfs -text
*.lzma filter=lfs diff=lfs merge=lfs -text
*.obscpio filter=lfs diff=lfs merge=lfs -text
*.oxt filter=lfs diff=lfs merge=lfs -text
*.pdf filter=lfs diff=lfs merge=lfs -text
*.png filter=lfs diff=lfs merge=lfs -text
*.rpm filter=lfs diff=lfs merge=lfs -text
*.tbz filter=lfs diff=lfs merge=lfs -text
*.tbz2 filter=lfs diff=lfs merge=lfs -text
*.tgz filter=lfs diff=lfs merge=lfs -text
*.ttf filter=lfs diff=lfs merge=lfs -text
*.txz filter=lfs diff=lfs merge=lfs -text
*.whl filter=lfs diff=lfs merge=lfs -text
*.xz filter=lfs diff=lfs merge=lfs -text
*.zip filter=lfs diff=lfs merge=lfs -text
*.zst filter=lfs diff=lfs merge=lfs -text

1
.gitignore vendored Normal file
View File

@ -0,0 +1 @@
.osc

11
_constraints Normal file
View File

@ -0,0 +1,11 @@
<?xml version="1.0" encoding="UTF-8"?>
<constraints>
<hardware>
<memoryperjob>
<size unit="M">900</size>
</memoryperjob>
<disk>
<size unit="G">4</size>
</disk>
</hardware>
</constraints>

3
coq-8.19.2.tar.gz Normal file
View File

@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:18035624bcda4f8cffe5f348e02f0ae2503af1c40de165788d7d45578e6c5725
size 7678311

3
coq-8.20.0.tar.gz Normal file
View File

@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:b08b364e6d420c58578d419247c5a710f4248bab962a46e542d452edac9e7914
size 7839432

3
coq-refman-8.19.2.tar.xz Normal file
View File

@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:d192cf2fd441f441cd4bd91672cd46ed1d8744bff132bace7aae3741ec4941de
size 7665520

3
coq-refman-8.20.0.tar.xz Normal file
View File

@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:7ff1da16e6483c7ea2ffc75b7254690041b206f4330b0ea02ef74b567a57fcf3
size 7788608

7
coq-rpmlintrc Normal file
View File

@ -0,0 +1,7 @@
# This line is mandatory to access the configuration functions
from Config import *
# Unfortunate choice, but we can't easily change that.
addFilter("hidden-file-or-dir .*/.coq-native")
# These are loaded manually by the OCaml runtime and need no dependency information.
addFilter("shared-library-without-dependency-information .*\.cmxs")

3
coq-stdlib-8.19.2.tar.xz Normal file
View File

@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:9f0a46efc7ec7365ebb03937ab25a6994eb4f405853a28122f7c55859afb290f
size 2176420

3
coq-stdlib-8.20.0.tar.xz Normal file
View File

@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:d0d9b5b24489633aa72fcaaddc462eb2d6f46ff55574c50fd520efb188dcfe7a
size 2203608

728
coq.changes Normal file
View File

@ -0,0 +1,728 @@
-------------------------------------------------------------------
Thu Sep 5 20:49:31 UTC 2024 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.20.0. The most impactful changes are:
* A mechanism to add user-defined rewrite rules to Coq's reduction
mechanisms; see chapter "User-defined rewrite rules".
* Support for primitive strings in terms.
* Reduction of the bytecode segment size, which in turn means
that `.vo` files might now be considerably smaller.
- Notable breaking changes:
* Syntactic global references passed through the `using` clauses
of `auto`-like tactics are now handled as plain references
rather than interpreted terms. In particular, their typeclass
arguments will not be inferred. In general, the previous
behaviour can be emulated by replacing `auto using foo` with
`pose proof foo; auto`.
* Argument order for the Ltac2 combinators `List.fold_left2` and
`List.fold_right2` changed to be the same as in OCaml.
* Importing a module containing a mutable Ltac2 definition does
not undo its mutations. Replace `Ltac2 mutable foo :=
some_expr.` with `Ltac2 mutable foo := some_expr. Ltac2 Set foo
:= some_expr.` to recover the previous behaviour.
* Some renaming in the standard library. Deprecations are
provided for a smooth transition.
- For more details, see the change log in coq-doc.
-------------------------------------------------------------------
Sun Jun 30 17:20:06 UTC 2024 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.19.2.
* Fixed a regression from Coq 8.18 in the presence of a defined
field in a primitive `Record`.
* Fixed an issue where the printer was sometimes failing to use a
prefix or infix custom notation whose right-hand side refers to
a different custom entry.
* Fixed `abstract` failure in the presence of admitted goals in
the surrounding proof.
* Fixed issues when using Ltac2 in VsCoq due to incorrect state
handling of Ltac2 notations.
* Fixed `Include` on a module containing a record declared with
`Primitive Projections`.
* Fixed an issue in `Fixpoint` with no arguments.
* Position error/warning tooltips correctly when multibyte UTF-8
characters are present.
-------------------------------------------------------------------
Thu Mar 7 22:31:46 UTC 2024 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.19.1.
* Fixed incorrect abstraction of sort variables for opaque
constants leading to an inconsistency.
* Fixed memory corruption with `vm_compute` (rare but more
likely with OCaml 5.1).
* "Found no matching notation to enable or disable" is now a
warning instead of an error.
* Fixed undeclared universe with multiple uses of `abstract`.
* Fixed incorrect printing of constructor values with multiple
arguments, and over-parenthesizing of constructor printing.
* Fixed incorrect declared type for Ltac2.FMap.fold.
-------------------------------------------------------------------
Sun Jan 28 20:20:35 UTC 2024 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.19.0. The most impactful changes:
* Sort polymorphism makes it possible to share common constructs
over `Type`, `Prop` and `SProp`.
* The notation `term%_scope` to set a scope only temporarily (in
addition to `term%scope` for opening a scope applying to all
subterms).
* `lazy`, `simpl`, `cbn` and `cbv` and the associated `Eval` and
`eval` reductions learned to do head reduction when given flag
`head`.
* New Ltac2 APIs, improved Ltac2 `exact` and dynamic building of
Ltac2 term patterns.
* New performance evaluation facilities: `Instructions` to count
CPU instructions used by a command and Profiling system to
produce trace files.
* New command `Attributes` to assign attributes such as
`deprecated` to a library file.
- Notable breaking changes:
* `replace` with `by tac` does not automatically attempt to solve
the generated equality subgoal using the hypotheses. Use `by
first [assumption | symmetry;assumption | tac]` if you need the
previous behaviour.
* Removed old deprecated files from the standard library.
- Use %fdupes in the documentation package.
-------------------------------------------------------------------
Sun Nov 12 22:52:11 UTC 2023 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Revert last change: this is now set in ocaml-rpm-macros.
- Increase stack size limit in QEMU user space builds. Here ulimit
has no effect, so we add a wrapper around ocamlopt.opt to PATH
that adds "-s ..." to the qemu-<arch> command line.
-------------------------------------------------------------------
Mon Oct 30 22:26:00 UTC 2023 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Increase stack size limit to fix build on riscv64.
-------------------------------------------------------------------
Sat Sep 16 20:35:51 UTC 2023 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.18.0.
* The default locality of `Hint` and `Instance` commands was
switched to `export`.
* The universe unification algorithm can now delay the commitment
to a sort (the algorithm used to pick `Type`). Thanks to this
feature many `Prop` and `SProp` annotations can be now omitted.
* Ltac2 supports array literals, maps and sets of primitive
datatypes such as names (of constants, inductive types, etc)
and fine-grained control over profiling.
* The warning system offers new categories, enabling finer
(de)activation of specific warnings. This should be
particularly useful to handle deprecations.
* Many new lemmas useful for teaching analysis with Coq are now
part of the standard library about real numbers.
* The `#[deprecated]` attribute can now be applied to definitions.
-------------------------------------------------------------------
Wed Jun 28 21:03:07 UTC 2023 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.17.1.
* Fixed incorrect paths emitted by coqdep in some cases for META
files which prevented dune builds for plugins from working
correctly.
* Fixed shadowing of record fields in extraction to OCaml.
* Fixed an impossible-to-turn-off debug message "backtracking and
redoing byextend on ...".
* Fixed a major memory regression affecting MathComp 2.
- Classify desktop entry under Science instead of Education.
- Add screenshot URL to AppStream metadata.
-------------------------------------------------------------------
Tue Mar 28 21:18:57 UTC 2023 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.17.0.
* Fixed a logical inconsistency due to `vm_compute` in presence
of side-effects in the enviroment (e.g. using Back or Fail).
* It is now possible to dynamically enable or disable notations.
* Support multiple scopes in `Arguments` and `Bind Scope`.
* The tactics chapter of the manual has many improvements in
presentation and wording. The documented grammar is semi-
automatically checked for consistency with the implementation.
* Fixes to the `auto` and `eauto` tactics, to respect hint
priorities and the documented use of simple apply. This is a
potentially breaking change.
* New Ltac2 APIs, deep pattern-matching with `as` clauses and
handling of literals, support for record types and preterms.
* Move from :> to :: syntax for declaring typeclass fields as
instances, fixing a confusion with declaration of coercions.
* Standard library improvements.
-------------------------------------------------------------------
Thu Jan 26 22:02:12 UTC 2023 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Build with ocaml-rpm-macros to get proper Requires and Provides
for coq-devel. This should prevent incompatibilities with other
Ocaml libraries when building native objects against coq-devel.
-------------------------------------------------------------------
Sat Nov 26 22:20:18 UTC 2022 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.16.1.
* Fixed the conversion of `Prod` values in the native compiler.
* Added `SProp` check for opaque names in conversion.
* Pass the correct environment to compute η-expansion of
cofixpoints in VM and native compilation.
* Fixed an inconsistency with conversion of primitive arrays, and
associated incomplete strong normalization of primitive arrays
with `lazy`.
* `Print Assumptions` treats opaque definitions with missing
proofs (as found in .vos files, produced using -vos) as axioms
instead of ignoring them.
-------------------------------------------------------------------
Thu Sep 8 21:11:24 UTC 2022 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.16.0.
* The guard checker (see `Guarded`) now ensures strong
normalization under any reduction strategy.
* Irrelevant terms (in the `SProp` sort) are now squashed to a
dummy value during conversion, fixing a subject reduction
issue and making proof conversion faster.
* Introduction of reversible coercions, which allow coercions
relying on meta-level resolution such as type-classes or
canonical structures. Also allow coercions that do not fullfill
the uniform inheritance condition.
* Generalized rewriting support for rewriting with `Type`-valued
relations and in `Type` contexts, using the
`Classes.CMorphisms` library.
* Added the boolean equality scheme command for decidable
inductive types.
* Added a `Print Notation` command.
* Incompatibilities in name generation for Program obligations,
`eauto` treatment of tactic failure levels, use of `ident` in
notations, parsing of module expressions.
* Standard library reorganization and deprecations.
* Improve the treatment of standard library numbers by
`Extraction`.
- Coq requires ocamlfind at runtime now.
-------------------------------------------------------------------
Wed Jun 1 21:41:11 UTC 2022 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.15.2.
* Tactics `intuition` and `dintuition` use
`Tauto.intuition_solver` (defined as `auto with *`) instead of
hardcoding `auto with *`. This makes it possible to change the
default solver with `Ltac Tauto.intuition_solver ::= ...`.
* Fixed an uncaught exception `UnableToUnify` with
bidirectionality hints.
* Fixed multiple CoqIDE bugs.
* Fixed an incorrect implementation of `SFClassify`, allowing for
a proof of `False` since 8.11.0, due to Axioms present in
`Float.Axioms`.
- Rename coq.desktop to fr.inria.coq.coqide.desktop as the
documentation suggests, add an accompanying metainfo file.
- Declare documentation as noarch.
-------------------------------------------------------------------
Thu Mar 24 22:56:21 UTC 2022 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.15.1.
* Fixes an inconsistency when using module subtyping with
inductive types.
* Speeds up CoqIDE on large files.
* Fixes a bug where `coqc -vok` was not creating a .vok file.
* Fixes a regression in `cbn`.
* Improves usability of schemes with `elim foo using scheme with
(P0 := ...)` (the `P0` name was not accessible in 8.15.0).
-------------------------------------------------------------------
Sat Jan 15 18:03:24 UTC 2022 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.15.0.
* The `apply with` tactic no longer renames arguments unless
the compatibility flag `Apply With Renaming` is set.
* Improvements to the `auto` tactic family, fixing `Hint Unfold`
behavior, and generalizing the use of discrimination nets.
* The `typeclasses eauto` tactic has a new `best_effort` option
allowing it to return partial solutions to a proof search
problem, depending on the mode declarations associated to each
constraint. This mode is used by typeclass resolution during
type inference to provide more precise error messages.
* Many commands and options were deprecated or removed after
deprecation and more consistently support locality attributes.
* The `Import` command is extended with `import_categories` to
select the components of a module to import or not, including
features such as hints, coercions, and notations.
* A visual Ltac debugger is now available in CoqIDE.
* For more details, see refman/changes.html in coq-doc.
-------------------------------------------------------------------
Sun Dec 12 20:11:15 UTC 2021 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.14.1.
* Fixed the implementation of persistent arrays used by the VM
and native compute so that it uses a uniform representation.
Previously, storing primitive floats inside primitive arrays
could cause memory corruption.
* Fixed missing registration of universe constraints in Module
Type elaboration.
* Made `abstract` more robust with respect to Ltac `constr`
bindings containing existential variables.
* Correct support of trailing `let` by tactic `specialize`.
* Fixed an anomaly with `Extraction Conservative Types` when
extracting pattern-matching on singleton types.
* Regular error instead of an anomaly when calling `Separate
Extraction` in a module.
-------------------------------------------------------------------
Wed Oct 20 21:31:46 UTC 2021 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.14.0.
* The internal representation of match has changed to a more
space-efficient and cleaner structure, allowing the fix of a
completeness issue with cumulative inductive types in the type-
checker. The internal representation is now closer to the user-
level view of match, where the argument context of branches and
the inductive binders in and as do not carry type annotations.
* A new coqnative binary performs separate native compilation of
libraries, starting from a .vo file. It is supported by
coq_makefile.
* Improvements to typeclasses and canonical structure resolution,
allowing more terms to be considered as classes or keys.
* More control over notations declarations and support for
primitive types in string and number notations.
* Removal of deprecated tactics, notably omega, which has been
replaced by a greatly improved lia, along with many bug fixes.
* New Ltac2 APIs for interaction with Ltac1, manipulation of
inductive types and printing.
* Many changes and additions to the standard library in the
numbers, vectors and lists libraries. A new signed primitive
integers library Sint63 is available in addition to the
unsigned Uint63 library.
* For more details, see refman/changes.html in coq-doc.
-------------------------------------------------------------------
Sat Sep 4 12:51:43 UTC 2021 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Add documentation package based on github.com/coq/doc until we
can build the documentation directly in OBS.
-------------------------------------------------------------------
Mon Apr 12 21:17:33 UTC 2021 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.13.2.
* Fix crash when using vm_compute on an irreducible PArray.set.
* Fix crash when loading .vo files containing a vm_compute
normalized primitive array.
* Fix Ltac2.Array.init computational complexity.
-------------------------------------------------------------------
Thu Feb 25 21:50:43 UTC 2021 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.13.1.
* Fix arities of VM opcodes for some floating-point operations
that could cause memory corruption.
-------------------------------------------------------------------
Sun Feb 7 22:48:00 UTC 2021 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.13.0.
* Introduction of primitive persistent arrays in the core
language, implemented using imperative persistent arrays.
* Introduction of definitional proof irrelevance for the equality
type defined in the SProp sort.
* Cumulative record and inductive type declarations can now
specify the variance of their universes.
* Various bugfixes and uniformization of behavior with respect to
the use of implicit arguments and the handling of existential
variables in declarations, unification and tactics.
* New warning for unused variables in catch-all match branches
that match multiple distinct patterns.
* New warning for Hint commands outside sections without a
locality attribute, whose goal is to eventually remove the
fragile default behavior of importing hints only when using
Require. The recommended fix is to declare hints as export,
instead of the current default global, meaning that they are
imported through Require Import only, not Require.
* General support for boolean attributes.
* Many improvements to the handling of notations, including
number notations, recursive notations and notations with
bindings. A new algorithm chooses the most precise notation
available to print an expression, which might introduce changes
in printing behavior.
* Tactic improvements in lia and its zify preprocessing step,
now supporting reasoning on boolean operators such as Z.leb and
supporting primitive integers Int63.
* Typing flags can now be specified per-constant / inductive.
* Improvements to the reference manual including updated syntax
descriptions that match Coq's grammar in several chapters, and
splitting parts of the tactics chapter to independent sections.
- Add build flag to turn off building of the IDE.
-------------------------------------------------------------------
Sun Dec 13 15:55:58 UTC 2020 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.12.2. Fixes two impacting 8.12 regressions:
* Fixed a regression causing notations mentioning a coercion to
be ignored.
* Fixed a regression causing incomplete inference of implicit
arguments in exists.
-------------------------------------------------------------------
Tue Nov 17 22:09:12 UTC 2020 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.12.1. This contains mostly bug fixes:
* Polymorphic side-effects inside monomorphic definitions were
incorrectly handled as not inlined. This allowed deriving an
inconsistency.
* Regression in error reporting after SSReflect's case tactic.
A generic error message "Could not fill dependent hole in
apply" was reported for any error following case or elim.
* Several bugs with Search.
* The details environment introduced in coqdoc in Coq 8.12 can
now be used as advertised in the reference manual.
* View menu "Display parentheses" introduced in CoqIDE in
Coq 8.12 now works correctly.
-------------------------------------------------------------------
Thu Aug 20 08:33:34 UTC 2020 - Martin Liška <mliska@suse.cz>
- Use memoryperjob constraint instead of %limit_build macro.
-------------------------------------------------------------------
Tue Jul 28 21:48:40 UTC 2020 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.12.0.
* New binder notation for non-maximal implicit arguments using []
allowing to set and see the implicit status of arguments
immediately.
* New notation Inductive "I A | x : s := ..." to distinguish the
uniform from the non-uniform parameters in inductive
definitions.
* More robust and expressive treatment of implicit inductive
parameters in inductive declarations.
* Improvements in the treatment of implicit arguments and
partially applied constants in notations, parsing of
hexadecimal number notation and better handling of scopes and
coercions for printing.
* A correct and efficient coercion coherence checking algorithm,
avoiding spurious or duplicate warnings.
* An improved Search command which accepts complex queries. This
takes precedence over the now deprecated ssreflect search.
* Many additions and improvements of the standard library.
* Improvements to the reference manual include a more logical
organization of chapters along with updated syntax descriptions
that match Coq's grammar in most but not all chapters.
-------------------------------------------------------------------
Sat Jun 6 12:11:06 UTC 2020 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.11.2.
* Fixed a kernel issue where using Require inside a section
caused an anomaly when closing the section.
* Fixed normalization in conclusion of custom induction scheme.
* Fixed a loss of location of some tactic errors.
* Ignore -native-compiler option when built without native
compute support.
* Fixed a segfault issue with CoqIDE completion.
* Highlighting style is now consistently applied to all three
buffers of CoqIDE.
-------------------------------------------------------------------
Wed Apr 8 22:20:23 UTC 2020 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.11.1, with upstream support for OCaml 4.10.
* Allow more inductive types in Unset Positivity Checking mode.
* Fixed bugs in dealing with precedence of notations in custom
entries.
* In primitive floats, print a warning when parsing a decimal
value that is not exactly a binary64 floating-point number.
For instance, parsing 0.1 will print a warning whereas parsing
0.5 won't.
* Fixed an issue in CoqIDE about compiling file paths containing
spaces.
* Fixed an issue where Extraction Implicit on the constructor of
a record was leading to an anomaly.
- Remove now obsolete ocaml-410-build.patch.
-------------------------------------------------------------------
Sun Mar 29 21:42:13 UTC 2020 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- The num library is required for OCaml 4.06 or later.
- Add ocaml-410-build.patch: fix build with OCaml 4.10.
-------------------------------------------------------------------
Thu Feb 6 16:38:09 UTC 2020 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.11.0.
* Ltac2, a new tactic language for writing more robust larger
scale tactics, with built-in support for datatypes and the
multi-goal tactic monad.
* Primitive floats are integrated in terms and follow the binary64
format of the IEEE 754 standard, as specified in the
Coq.Float.Floats library.
* Many other cleanups and improvements have been performed and
are further described in the changelog.
* Special note on compatibility: Fixed bugs of Export and Import
that can have a significant impact on user developments.
- Drop unneeded empty *.vos files.
-------------------------------------------------------------------
Sat Nov 30 16:40:21 UTC 2019 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.10.2.
* Fixed a critical bug of template polymorphism and nonlinear
universes;
* Fixed a few anomalies;
* Fixed an 8.10 regression related to the printing of coercions
associated to notations;
* Fixed uneven dimensions of CoqIDE panels when window has been
resized;
* Fixed queries in CoqIDE.
-------------------------------------------------------------------
Tue Nov 12 22:46:34 UTC 2019 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.10.0.
* some quality-of-life bug fixes;
* a critical bug fix related to template polymorphism;
* native 63-bit machine integers;
* a new sort of definitionally proof-irrelevant propositions: SProp;
* private universes for opaque polymorphic constants;
* string notations and numeral notations;
* a new simplex-based proof engine for the tactics lia, nia, lra
and nra;
* new introduction patterns for SSReflect;
* a tactic to rewrite under binders: under;
* easy input of non-ASCII symbols in CoqIDE, which now uses GTK3.
- Update to version 8.10.1.
* Fix proof of False when using SProp
* Fix an anomaly when unsolved evar in Add Ring
* Fix Ltac regression in binding free names in uconstr
* Fix handling of unicode input before space
* Fix custom extraction of inductives to JSON
- Update version requirements.
-------------------------------------------------------------------
Tue Nov 12 22:31:20 UTC 2019 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Fix findlib build dependency.
-------------------------------------------------------------------
Sun Nov 3 18:06:05 UTC 2019 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Use memory-constraints package to limit number of threads.
- Add dependencies to fix installation issues.
-------------------------------------------------------------------
Wed Sep 25 20:16:34 UTC 2019 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Prevent OOM by limiting the number of threads.
-------------------------------------------------------------------
Tue Sep 24 22:13:12 UTC 2019 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Change license tag to LGPL-2.1-only.
- Remove obsolete %defattr and other spec-cleaner suggestions.
-------------------------------------------------------------------
Sat Aug 3 13:22:18 UTC 2019 - Aaron Puchert <aaronpuchert@alice-dsl.net>
- Update to version 8.9.0.
* Kernel: mutually recursive records are now supported.
* Notations:
+ Support for autonomous grammars of terms called “custom
entries”.
+ Deprecated notations of the standard library will be removed
in the next version of Coq, see the next subsection for a
script to ease porting.
+ Added the "Numeral Notation" command for registering decimal
numeral notations for custom types.
* Tactics: Introduction tactics intro/intros on a goal that is an
existential variable now force a refinement of the goal into a
dependent product rather than failing.
* Decision procedures: deprecation of tactic romega in favor of
lia and removal of fourier, replaced by lra which subsumes it.
* Proof language: focusing bracket { now supports named goals,
e.g. [x]:{ will focus on a goal (existential variable) named x.
* SSReflect: the implementation of delayed clear was simplified:
the variables are always renamed using inaccessible names when
the clear switch is processed and finally cleared at the end of
the intro pattern. In addition to that, the use-and-discard
flag {} typical of rewrite rules can now be also applied to
views, e.g. => {}/v applies v and then clears v.
See Section Introduction in the context.
* Vernacular:
+ Experimental support for attributes on commands, as in
"#[local] Lemma foo : bar". Tactics and tactic notations now
support the deprecated attribute.
+ Removed deprecated commands "Arguments Scope" and "Implicit
Arguments" in favor of "Arguments (scopes)" and "Arguments
(implicits)".
+ New flag "Uniform Inductive Parameters" to avoid repeating
uniform parameters in constructor declarations.
+ New commands "Hint Variables" and "Hint Constants" for
controlling the opacity status of variables and constants in
hint databases. It is recommended to always use these
commands after creating a hint database with Create HintDb.
+ Multiple sections with the same name are now allowed.
* Library: additions and changes in the VectorDef, Ascii, and
String libraries. Syntax notations are now available only when
using "Import" of libraries and not merely "Require".
(Source of incompatibility, see Change Log for details)
* Toplevels: coqtop and coqide can now display diffs between
proof steps in color, using the Diffs option.
* Documentation: we integrated a large number of fixes to the new
Sphinx documentation.
* Tools: removed gallina utility and homebrewed Emacs mode.
- Update to version 8.9.1, which contains
* some quality-of-life bug fixes,
* many improvements to the documentation,
* a critical bug fix related to primitive projections and
native_compute.
- Remove unnecessary dependencies: ncurses-devel is no longer
needed, and the docs aren't build with TeX and hevea anymore.
- Remove dependencies that are automatically detected.
- Remove icon that is also available from the tarball.
- Replace some identical files by symlinks.
- Fix executable bits and shebangs.
- Separate runtime from devel files by ending.
- Use %license for LICENSE and CREDITS.
- Be more explicit in %files.
- Add mime type for Coq source files so they open with the IDE.
- Add rpmlintrc for issues that are hard to fix.
-------------------------------------------------------------------
Thu Oct 11 09:35:41 UTC 2018 - ptrommler@icloud.com
- update to 8.8.2
-------------------------------------------------------------------
Sun Jan 7 10:41:00 UTC 2018 - ptrommler@icloud.com
- update to 8.7.1
-------------------------------------------------------------------
Thu Nov 2 15:32:20 UTC 2017 - ptrommler@icloud.com
- update to 8.7.0
* I need this in class b/c coq-ide reads _CoqProject files
-------------------------------------------------------------------
Thu Apr 13 11:34:12 UTC 2017 - peter.trommler@ohm-hochschule.de
- update to 8.6 from upstream
-------------------------------------------------------------------
Fri Dec 2 14:30:06 UTC 2016 - peter.trommler@ohm-hochschule.de
- update to 8.5pl3 from upstream
-------------------------------------------------------------------
Fri Oct 21 18:11:31 UTC 2016 - peter.trommler@ohm-hochschule.de
- update to 8.5pl2 from upstream
-------------------------------------------------------------------
Sun Apr 10 10:32:12 UTC 2016 - peter.trommler@ohm-hochschule.de
- update to 8.5 from upstream
-------------------------------------------------------------------
Sat May 31 18:46:45 UTC 2014 - peter.trommler@ohm-hochschule.de
- update to 8.4pl4 from upstream
-------------------------------------------------------------------
Sun Jan 12 11:17:04 UTC 2014 - peter.trommler@ohm-hochschule.de
- update to 8.4pl3 from upstream
- follow upstream versioning
-------------------------------------------------------------------
Sun Nov 10 08:45:53 UTC 2013 - peter.trommler@ohm-hochschule.de
- revert to our own lablgtk on older systems
* coq-ide cannot be built using 12.2 lablgtk2
-------------------------------------------------------------------
Wed Nov 6 19:53:49 UTC 2013 - peter.trommler@ohm-hochschule.de
- use system provided lablgtk2
-------------------------------------------------------------------
Mon Apr 8 11:31:02 UTC 2013 - peter.trommler@ohm-hochschule.de
- update to 8.4pl2
- coqtop: handle interrupt signals reliably
- restor old behavior for code extraction (AccessOpaque)
-------------------------------------------------------------------
Wed Dec 26 19:49:24 UTC 2012 - peter.trommler@ohm-hochschule.de
- update to 8.4pl1 from upstream
- dropped f0b93...055.patch (integrated upstream)
- use ocamlfind to find lablgtk2
-------------------------------------------------------------------
Mon Dec 3 10:14:09 UTC 2012 - peter.trommler@ohm-hochschule.de
- add patch for lablgtk2 v 2.16
-------------------------------------------------------------------
Thu Nov 29 20:18:17 UTC 2012 - peter.trommler@ohm-hochschule.de
- mark config file
-------------------------------------------------------------------
Sun Nov 11 18:53:41 UTC 2012 - peter.trommler@ohm-hochschule.de
- give up on old ocaml names and require ocaml-lablgtk2-devel
- clean up spec file
-------------------------------------------------------------------
Thu Oct 18 13:28:32 UTC 2012 - peter.trommler@ohm-hochschule.de
- remove requires and rely on automatic dependency generation
for ocaml
-------------------------------------------------------------------
Wed Oct 17 16:01:25 UTC 2012 - peter.trommler@ohm-hochschule.de
- packaged new file coq.png
-------------------------------------------------------------------
Sun Oct 7 15:59:53 UTC 2012 - peter.trommler@ohm-hochschule.de
- update to 8.4 from upstream
-------------------------------------------------------------------
Thu Apr 12 12:14:04 UTC 2012 - peter.trommler@ohm-hochschule.de
- add ocaml- prefix to lablgtk-devel Buildrequires
-------------------------------------------------------------------
Wed Apr 11 17:32:25 UTC 2012 - peter.trommler@ohm-hochschule.de
- add Buildrequires hevea needed for documentation
-------------------------------------------------------------------
Wed Apr 11 16:56:52 UTC 2012 - peter.trommler@ohm-hochschule.de
- cleaned up spec file (BuildRequires and Requires one each line)
- SPDX license tag
-------------------------------------------------------------------
Wed Apr 11 16:26:24 UTC 2012 - peter.trommler@ohm-hochschule.de
- upgraded to 8.3pl4 from upstream
Bug fixes:
- #2724 (using notations with binders in cases patterns was provoking an anomaly)
- #2723 (alpha-conversion bug #2723 introduced in r12485-12486)
- #2732 (anomaly when using the tolerance for writing "f atomic_tac"
as a short-hand for "f ltac:(atomic_tac)")
- #2729 (vm_compute: function used to decompose constructors did not handle let-ins)
- #2728 (compatibility with camlp5 6.05)
- #2682 (Fail discard the effects of a successful command)
- #2703 (Undetected universe inconsistency)
- #2667 (Coq crashes when "Arguments Scope" has too many parameters)
- Compilation of coqide under MacOS with gtk >= 2.24.11
- Coqdoc: Fixing missing newline when using "Proof term."

275
coq.spec Normal file
View File

@ -0,0 +1,275 @@
#
# spec file for package coq
#
# Copyright (c) 2024 SUSE LLC
# Copyright (c) 2012-2018 Peter Trommler, peter.trommler at ohm-hochschule.de
# Copyright (c) 2024 Aaron Puchert <aaronpuchert@alice-dsl.net>
#
# All modifications and additions to the file contributed by third parties
# remain the property of their copyright owners, unless otherwise agreed
# upon. The license for this file, and modifications and additions to the
# file, is the same license as for the pristine package itself (unless the
# license for the pristine package is not an Open Source License, in which
# case the license is the MIT License). An "Open Source License" is a
# license that conforms to the Open Source Definition (Version 1.9)
# published by the Open Source Initiative.
# Please submit bugfixes or comments via https://bugs.opensuse.org/
#
%bcond_without ide
%global dune_packages coq,coq-core,coq-stdlib
%if %{with ide}
%global dune_packages %{dune_packages},coqide,coqide-server
%endif
Name: coq
Version: 8.20.0
Release: 0
Summary: Proof Assistant based on the Calculus of Inductive Constructions
License: LGPL-2.1-only
Group: Productivity/Scientific/Math
URL: https://coq.inria.fr/
Source: https://github.com/coq/coq/archive/V%{version}.tar.gz#/%{name}-%{version}.tar.gz
Source1: fr.inria.coq.coqide.desktop
Source2: fr.inria.coq.coqide.metainfo.xml
Source3: coq.xml
Source50: coq-refman-%{version}.tar.xz
Source51: coq-stdlib-%{version}.tar.xz
Source100: %{name}-rpmlintrc
BuildRequires: desktop-file-utils
BuildRequires: fdupes
BuildRequires: make >= 3.81
BuildRequires: ocaml >= 4.09.0
BuildRequires: ocaml-camlp5-devel >= 5.08
BuildRequires: ocaml-dune >= 3.6.1
BuildRequires: ocaml-rpm-macros
BuildRequires: ocamlfind(findlib)
BuildRequires: ocamlfind(zarith)
%if %{with ide}
BuildRequires: update-desktop-files
BuildRequires: ocamlfind(lablgtk3-sourceview3)
%endif
Requires: ocamlfind
%description
Proof assistant which allows to handle calculus assertions, check mechanically
proofs of these assertions, helps to find formal proofs and extracts a certified
program from the constructive proof of its formal specification.
This package contains shared files and the command line interface.
For a graphical interface install %{name}-ide.
%package ide
Summary: IDE for The Coq Proof Assistant
Group: Productivity/Scientific/Math
Requires: %{name} = %{version}
%description ide
The Coq Integrated Development Interface is a graphical interface for the Coq proof assistant.
%package devel
Summary: Development files for coq
Group: Development/Libraries/Other
Requires: %{name} = %{version}
Requires: ocaml >= 4.09.0
%description devel
This package contains development files for Coq.
%package doc
Summary: Documentation for coq
Group: Documentation/HTML
Requires: %{name} = %{version}
BuildArch: noarch
%description doc
HTML reference manual for Coq and full documentation of the standard library.
%prep
%setup -q -a 50 -a 51
%build
%if 0%{?qemu_user_space_build}
# The OCaml compiler sometimes needs a bit more stack than the usual limit.
# While ocaml-rpm-macros increases the limit, this doesn't affect a QEMU build.
# We add a wrapper script to PATH. This doesn't affect the processes started by
# Dune, but coqc itself uses the compiler from PATH.
mkdir bin
echo "#!/bin/bash
exec /usr/bin/qemu-%{_host_cpu} -s $((64*1024*1024)) /usr/bin/ocamlopt.opt \"\$@\"" >bin/ocamlopt.opt
chmod +x bin/ocamlopt.opt
export PATH=$PWD/bin:$PATH
%endif
export CFLAGS='%{optflags}'
./configure \
-prefix %{_prefix} \
-libdir %{_libdir}/coq \
-mandir %{_mandir} \
-datadir %{_datadir}/%{name} \
-docdir %{_docdir}/%{name} \
-configdir %{_sysconfdir}/xdg/%{name} \
-native-compiler yes \
-natdynlink yes \
-browser "xdg-open %s"
make %{?_smp_mflags} dunestrap
dune_release_pkgs='%{dune_packages}'
%ocaml_dune_setup
%ocaml_dune_build
%install
%global ocaml_standard_library %{_libdir}
%ocaml_dune_install
%if %{with ide}
%suse_update_desktop_file -i %{SOURCE1}
install -D -m 644 %{SOURCE1} %{buildroot}%{_datadir}/applications/fr.inria.coq.coqide.desktop
install -D -m 644 %{SOURCE2} %{buildroot}%{_datadir}/metainfo/fr.inria.coq.coqide.metainfo.xml
install -D -m 644 %{SOURCE3} %{buildroot}%{_datadir}/mime/packages/coq.xml
mkdir -p %{buildroot}%{_datadir}/icons/hicolor/256x256/apps
ln -s %{_datadir}/coq/coq.png %{buildroot}%{_datadir}/icons/hicolor/256x256/apps/coq.png
%endif
# Sometimes we get identical x and x.opt files, replace by symlink x -> x.opt.
for bin in %{buildroot}%{_bindir}/*.opt
do
if [ -f ${bin%.opt} ] && diff $bin ${bin%.opt}
then
rm ${bin%.opt}
ln -s ${bin#%{buildroot}} ${bin%.opt}
fi
done
# Fix executable bit and shebangs, preferring python3.
# (https://www.python.org/dev/peps/pep-0394/#for-python-runtime-distributors)
chmod -x %{buildroot}%{_libdir}/coq-core/tools/TimeFileMaker.py
sed -i '1s|^#!/usr/bin/env *|#!/usr/bin/|;1s|^#!/usr/bin/python$|#!/usr/bin/python3|' \
%{buildroot}%{_libdir}/coq-core/tools/make-{one-time-file,both-{time,single-timing}-files}.py
# Remove superfluous man page.
rm %{buildroot}%{_mandir}/man1/coqtop.byte.1
# Remove unneeded empty *.vos files.
find %{buildroot}%{_libdir}/coq -empty -name '*.vos' -delete
# Build lists of runtime and devel files by ending.
# Compiled theories and shared objects are needed at runtime.
find %{buildroot}%{_libdir} -type d | sed "s|%{buildroot}|%%dir |g" >dir.list
sed -i '1d; /coq-core\/tools/d' dir.list
find %{buildroot}%{_libdir} -name '*.cmxs' \
-or -name '*.so' \
-or -name '*.vo' | sed "s|%{buildroot}||g" >runtime.list
# Object files, static libraries and import definitions are only needed for development.
# For now, we also put the standard library Coq sources here, since the runtime
# package contains the HTML documentation for the standard library.
find %{buildroot}%{_libdir} -name '*.a' \
-or -name '*.cma' \
-or -name '*.cmi' \
-or -name '*.cmt' \
-or -name '*.cmti' \
-or -name '*.cmx' \
-or -name '*.cmxa' \
-or -name '*.glob' \
-or -name '*.ml' \
-or -name '*.mli' \
-or -name '*.o' \
-or -name '*.v' | sed "s|%{buildroot}||g" >devel.list
# Until we can build it, we fetch the documentation from the official website:
# git clone --filter=tree:0 --sparse https://github.com/coq/doc.git
# pushd doc
# git sparse-checkout add V%{version}
# cd V%{version}
# tar --sort=name --owner=0 --group=0 --mtime="@${SOURCE_DATE_EPOCH}" \
# --pax-option=exthdr.name=%d/PaxHeaders/%f,delete=atime,delete=ctime \
# -cJf ../../coq-refman-%{version}.tar.xz refman
# tar --sort=name --owner=0 --group=0 --mtime="@${SOURCE_DATE_EPOCH}" \
# --pax-option=exthdr.name=%d/PaxHeaders/%f,delete=atime,delete=ctime \
# -cJf ../../coq-stdlib-%{version}.tar.xz stdlib
# popd
# Drop some CSS files and headers in stdlib documentation, add some margin directly.
find stdlib/ -name '*.html' -exec sed -i '
s#//coq.inria.fr/sites/all/themes/coq/coqdoc.css#%{_libdir}/coq-core/tools/coqdoc/coqdoc.css#
/<link type="text\/css" rel="stylesheet" media="all" href="\/\/coq.inria.fr\/.*.css" \/>/d
/<div id="container">/s/>/ style="margin:1em;">/
/^ <div id="headertop">$/,/^ <\/div>$/d
/^ <div id="header">$/,/^ <\/div>$/d
' {} +
mkdir -p %{buildroot}%{_docdir}/%{name}
cp -r refman stdlib %{buildroot}%{_docdir}/%{name}
rm -r %{buildroot}%{_docdir}/%{name}/refman/{.buildinfo,.doctrees,_sources}
%fdupes %{buildroot}%{_docdir}/%{name}
%files -f dir.list -f runtime.list
%license LICENSE CREDITS
%{_bindir}/coq-tex
%{_bindir}/coq_makefile
%{_bindir}/coqc
%{_bindir}/coqc.byte
%{_bindir}/coqchk
%{_bindir}/coqdep
%{_bindir}/coqdoc
%{_bindir}/coqnative
%{_bindir}/coqpp
%{_bindir}/coqtimelog2html
%{_bindir}/coqtop
%{_bindir}/coqtop.byte
%{_bindir}/coqwc
%{_bindir}/coqworker.opt
%{_bindir}/coqworkmgr
%{_bindir}/csdpcert
%{_bindir}/ocamllibdep
%{_bindir}/votour
%{_libdir}/coq-core/tools
%exclude %{_libdir}/coq-core/tools/CoqMakefile.in
%{_mandir}/man1/coq-tex.1%{ext_man}
%{_mandir}/man1/coq_makefile.1%{ext_man}
%{_mandir}/man1/coqc.1%{ext_man}
%{_mandir}/man1/coqchk.1%{ext_man}
%{_mandir}/man1/coqdep.1%{ext_man}
%{_mandir}/man1/coqdoc.1%{ext_man}
%{_mandir}/man1/coqnative.1%{ext_man}
%{_mandir}/man1/coqtop.1%{ext_man}
%{_mandir}/man1/coqwc.1%{ext_man}
%dir %{_datadir}/texmf
%dir %{_datadir}/texmf/tex
%dir %{_datadir}/texmf/tex/latex
%dir %{_datadir}/texmf/tex/latex/misc
%{_datadir}/texmf/tex/latex/misc/coqdoc.sty
%if %{with ide}
%files ide
%{_bindir}/coqide
%{_bindir}/coqidetop.byte
%{_bindir}/coqidetop.opt
%{_mandir}/man1/coqide.1%{ext_man}
%{_datadir}/%{name}
%{_datadir}/applications/fr.inria.coq.coqide.desktop
%{_datadir}/icons/hicolor/256x256/apps/coq.png
%{_datadir}/metainfo/fr.inria.coq.coqide.metainfo.xml
%{_datadir}/mime/packages/coq.xml
%endif
%files devel -f dir.list -f devel.list
%{_libdir}/coq-core/revision
%{_libdir}/coq-core/dev/ml_toplevel
%{_libdir}/{%{dune_packages}}/{META,dune-package,opam}
%{_libdir}/coq-core/tools/CoqMakefile.in
%files doc
%dir %{_docdir}/%{name}
%{_docdir}/%{name}/refman
%{_docdir}/%{name}/stdlib
%changelog

12
coq.xml Normal file
View File

@ -0,0 +1,12 @@
<?xml version="1.0" encoding="UTF-8"?>
<mime-info xmlns="http://www.freedesktop.org/standards/shared-mime-info">
<mime-type type="text/x-coqsrc">
<comment xml:lang="en">Coq source file</comment>
<glob pattern="*.v"/>
<icon name="coq"/>
</mime-type>
<mime-type type="application/x-coq-object">
<comment xml:lang="en">Coq object file</comment>
<glob pattern="*.vo"/>
</mime-type>
</mime-info>

10
fr.inria.coq.coqide.desktop Normal file
View File

@ -0,0 +1,10 @@
[Desktop Entry]
Encoding=UTF-8
Type=Application
Name=Coq IDE
GenericName=Proof Assistant
Comment=Proof Assistant based on the Calculus of Inductive Constructions
Categories=Science;Math;
MimeType=text/x-coqsrc;
Exec=coqide %F
Icon=coq

71
fr.inria.coq.coqide.metainfo.xml Normal file
View File

@ -0,0 +1,71 @@
<?xml version="1.0" encoding="UTF-8"?>
<component>
<id type="desktop">fr.inria.coq.coqide</id>
<metadata_license>CC0-1.0</metadata_license>
<name>Coq IDE</name>
<summary>Graphical frontend for the Coq formal proof management system</summary>
<description>
<p>
Coq implements a program specification and mathematical higher-level language called <em>Gallina</em> that is based on an expressive formal language called the <em>Calculus of Inductive Constructions</em> that itself combines both a higher-order logic and a richly-typed functional programming language.
Through a <em>vernacular</em> language of commands, Coq allows:
</p>
<ul>
<li>to define functions or predicates, that can be evaluated efficiently;</li>
<li>to state mathematical theorems and software specifications;</li>
<li>to interactively develop formal proofs of these theorems;</li>
<li>to machine-check these proofs by a relatively small certification "kernel";</li>
<li>to extract certified programs to languages like OCaml, Haskell or Scheme.</li>
</ul>
<p>
As a proof development system, Coq provides interactive proof methods, decision and semi-decision algorithms, and a <em>tactic</em> language for letting the user define its own proof methods.
Connection with external computer algebra system or theorem provers is available.
</p>
<p>
As a platform for the formalization of mathematics or the development of programs, Coq provides support for high-level notations, implicit contents and various other useful kinds of macros.
</p>
</description>
<categories>
<category>Development</category>
<category>IDE</category>
<category>Science</category>
<category>ComputerScience</category>
<category>Math</category>
</categories>
<keywords>
<keyword>dependent-types</keyword>
<keyword>coq</keyword>
<keyword>theorem-proving</keyword>
<keyword>proof-assistant</keyword>
</keywords>
<url type="homepage">https://coq.inria.fr/</url>
<url type="bugtracker">https://github.com/coq/coq/issues</url>
<url type="faq">https://github.com/coq/coq/wiki/The-Coq-FAQ</url>
<url type="help">https://coq.inria.fr/refman/practical-tools/coqide.html</url>
<url type="donation">https://coq.inria.fr/consortium</url>
<url type="vcs-browser">https://github.com/coq/coq</url>
<url type="contribute">https://github.com/coq/coq/blob/master/CONTRIBUTING.md</url>
<launchable type="desktop-id">fr.inria.coq.coqide.desktop</launchable>
<releases>
<release version="8.19.1" date="2024-03-04"/>
<release version="8.19.0" date="2024-01-24"/>
<release version="8.18.0" date="2023-09-08"/>
<release version="8.17.1" date="2023-06-27"/>
<release version="8.17.0" date="2023-03-27"/>
<release version="8.16.1" date="2022-11-25"/>
<release version="8.16.0" date="2022-09-05"/>
<release version="8.15.2" date="2022-05-31"/>
<release version="8.15.1" date="2022-03-22"/>
</releases>
<provides>
<binary>coqide</binary>
</provides>
<project_license>LGPL-2.1-only</project_license>
<screenshots>
<screenshot type="default">
<image type="source">
https://coq.inria.fr/refman/_images/coqide.png
</image>
</screenshot>
</screenshots>
<content_rating type="oars-1.1"/>
</component>