-
Notifications
You must be signed in to change notification settings - Fork 166
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #3212 from DmxLarchey/Kruskal-Fan-Higman+Karp-Miller
New release for Kruskal-[Higman,Fan] and Kar-Miller for SWHID archival
- Loading branch information
Showing
3 changed files
with
121 additions
and
0 deletions.
There are no files selected for viewing
41 changes: 41 additions & 0 deletions
41
released/packages/coq-karp-miller/coq-karp-miller.1.1/opam
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,41 @@ | ||
opam-version: "2.0" | ||
synopsis: "Certified Karp-Miller algorithm for the covering of Petri nets" | ||
description: """ | ||
Based on the Kruskal-AlmostFull library, we build two correct by construction Karp-Miller | ||
algorithms: the first one decides for the coverability problem; and the second one, a | ||
refined version, builds the Karp-Miller tree and, either a path in that tree giving a covering, | ||
or a proof that no such path exists in the Karp-Miller trees. | ||
""" | ||
maintainer: ["Dominique Larchey-Wendling (https://github.com/DmxLarchey)"] | ||
authors: "Dominique Larchey-Wendling (https://github.com/DmxLarchey)" | ||
license: "MPL-2.0" | ||
homepage: "https://github.com/DmxLarchey/Karp-Miller/" | ||
bug-reports: "https://github.com/DmxLarchey/Karp-Miller/issues" | ||
dev-repo: "git+https://github.com:DmxLarchey/Karp-Miller/" | ||
|
||
build: [ | ||
[make "-j%{jobs}%"] | ||
] | ||
install: [ | ||
[make "install"] | ||
] | ||
|
||
depends: [ | ||
"coq-kruskal-almostfull" {>= "1.2"} | ||
"coq-kruskal-trees" {} | ||
"coq-kruskal-finite" {} | ||
] | ||
|
||
url { | ||
src: "https://github.com/DmxLarchey/Karp-Miller/releases/download/1.1/Karp-Miller-1.1.tar.gz" | ||
checksum: [ | ||
"sha256=240c7b0788df232d448c395241a7825feffb9c337d17cf3d3039708a9fcfbc4b" | ||
] | ||
} | ||
|
||
tags: [ | ||
"category:Computer Science/Data Types and Data Structures" | ||
"date:2024-11-22" | ||
"logpath:KarpMiller" | ||
] | ||
|
39 changes: 39 additions & 0 deletions
39
released/packages/coq-kruskal-fan/coq-kruskal-fan.1.2/opam
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,39 @@ | ||
opam-version: "2.0" | ||
synopsis: "Extending Coq library for manipulating Almost Full relations with the FAN theorem" | ||
description: """ | ||
This library formalizes additional tools for AF relations, the FAN theorem for inductive bars | ||
and a constructive variant of König's lemma. | ||
""" | ||
maintainer: ["Dominique Larchey-Wendling (https://github.com/DmxLarchey)"] | ||
authors: "Dominique Larchey-Wendling (https://github.com/DmxLarchey)" | ||
license: "MPL-2.0" | ||
homepage: "https://github.com/DmxLarchey/Kruskal-Higman/" | ||
bug-reports: "https://github.com/DmxLarchey/Kruskal-Higman/issues" | ||
dev-repo: "git+https://github.com:DmxLarchey/Kruskal-Higman/" | ||
|
||
build: [ | ||
[make "-j%{jobs}%" "type"] | ||
] | ||
install: [ | ||
[make "install"] | ||
] | ||
|
||
depends: [ | ||
"coq-kruskal-trees" {>= "1.4"} | ||
"coq-kruskal-finite" {>= "1.4"} | ||
"coq-kruskal-almostfull" {>= "1.1"} | ||
] | ||
|
||
url { | ||
src: "https://github.com/DmxLarchey/Kruskal-Fan/releases/download/1.2/Kruskal-Fan-1.2.tar.gz" | ||
checksum: [ | ||
"sha256=dbd107c4afa5b01a94f69b49f6c33dc7249396865bad9bf82367d5ec49d92c09" | ||
] | ||
} | ||
|
||
tags: [ | ||
"category:Computer Science/Data Types and Data Structures" | ||
"date:2024-11-22" | ||
"logpath:KruskalFanProp" | ||
"logpath:KruskalFanType" | ||
] |
41 changes: 41 additions & 0 deletions
41
released/packages/coq-kruskal-higman/coq-kruskal-higman.1.3/opam
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,41 @@ | ||
opam-version: "2.0" | ||
synopsis: "Extending Coq library for manipulating Almost Full relations with Higman's lemma" | ||
description: """ | ||
This library formalizes additional tools for AF relations, eg quasi morphisms applied to Higman's lemma. | ||
""" | ||
maintainer: ["Dominique Larchey-Wendling (https://github.com/DmxLarchey)"] | ||
authors: "Dominique Larchey-Wendling (https://github.com/DmxLarchey)" | ||
license: "MPL-2.0" | ||
homepage: "https://github.com/DmxLarchey/Kruskal-Higman/" | ||
bug-reports: "https://github.com/DmxLarchey/Kruskal-Higman/issues" | ||
dev-repo: "git+https://github.com:DmxLarchey/Kruskal-Higman/" | ||
|
||
build: [ | ||
[make "-j%{jobs}%" "type"] | ||
] | ||
install: [ | ||
[make "install"] | ||
] | ||
|
||
depends: [ | ||
"coq-kruskal-trees" | ||
"coq-kruskal-finite" | ||
"coq-kruskal-almostfull" | ||
"coq-kruskal-fan" | ||
] | ||
|
||
|
||
url { | ||
src: "https://github.com/DmxLarchey/Kruskal-Higman/releases/download/1.3/Kruskal-Higman-1.3.tar.gz" | ||
checksum: [ | ||
"sha256=4dd079239f71bb4827b8dfdd6c33bbecb72e4e8be4379ab8bd0e1a6e5beaad06" | ||
] | ||
} | ||
|
||
tags: [ | ||
"category:Computer Science/Data Types and Data Structures" | ||
"date:2024-11-22" | ||
"logpath:KruskalHigmanProp" | ||
"logpath:KruskalHigmanType" | ||
] | ||
|