fblanqui / color Goto Github PK

View Code? Open in Web Editor NEW

33.0 33.0 21.0 4.22 MB

Coq library on rewriting theory and termination

License: Other

Makefile 0.05% Coq 99.76% OCaml 0.06% Shell 0.11% Awk 0.01%

color's People

Contributors

Stargazers

Watchers

color's Issues

Links to old GForge opam versions

Hello,

The links in the opam packages for versions prior to 1.8 do not seem to work anymore. For example, in https://github.com/coq/opam-coq-archive/blob/master/released/packages/coq-color/coq-color.1.7.0/opam there is a link to https://gforge.inria.fr/frs/download.php/file/38188/color.1.7.0.tar.gz which returns "403 Forbidden" on my computer.

The INSTALL file still indicates compatibility with Coq 8.7

But the testing has moved to v8.8 / master only.

`fix` tactic without a name is deprecated.

The tactic form fix N where N is a number is deprecated as it depends on the name of the current lemma.

See coq/coq#7196.

The backwards compatible fix is to use fix name_of_the_fixpoint N.

Affected lines in color:

Coccinelle/basis/decidable_set.v:68:fix 1; intros [ | n1] [ | n2]; simpl; try reflexivity; try discriminate.
Coccinelle/basis/ordered_set.v:109:fix 1.
Coccinelle/basis/ordered_set.v:127:unfold o; fix 1.
Coccinelle/examples/cime_trace/equational_extension.v:147:  fix 3.
Coccinelle/list_extensions/dickson.v:556:fix 1.
Coccinelle/list_extensions/dickson.v:1006:fix 1.
Coccinelle/list_extensions/list_permut.v:1093:fix 1.
Coccinelle/list_extensions/list_permut.v:1223:fix 1.
Coccinelle/list_extensions/list_permut.v:1248:fix 1.
Coccinelle/list_extensions/list_permut.v:1393:fix 1.
Coccinelle/list_extensions/list_set.v:84:unfold without_red; fix 2.
Coccinelle/list_extensions/list_set.v:101:unfold without_red; fix 2.
Coccinelle/list_extensions/list_set.v:118:unfold without_red; fix 2.
Coccinelle/list_extensions/list_set.v:139:unfold without_red; fix 1.
Coccinelle/list_extensions/list_set.v:173:fix 2.
Coccinelle/list_extensions/list_set.v:185:fix 2.
Coccinelle/list_extensions/list_set.v:200:unfold without_red; fix 1.
Coccinelle/list_extensions/list_set.v:311:unfold without_red; fix 2.
Coccinelle/list_extensions/list_set.v:427:fix 2.
Coccinelle/list_extensions/list_set.v:444:fix 2.
Coccinelle/list_extensions/list_set.v:492:fix 2.
Coccinelle/list_extensions/list_set.v:641:revert l1 l2; fix 1.
Coccinelle/list_extensions/list_set.v:899:fix 1.
Coccinelle/list_extensions/list_set.v:943:fix 3.
Coccinelle/list_extensions/list_set.v:997:fix 1.
Coccinelle/list_extensions/list_sort.v:367:fix 1.
Coccinelle/list_extensions/more_list.v:176:fix 4.
Coccinelle/list_extensions/more_list.v:209:intros A B f; fix 1.
Coccinelle/list_extensions/more_list.v:371:fix 3.
Coccinelle/list_extensions/more_list.v:386:fix 2.
Coccinelle/list_extensions/more_list.v:427:fix 1; intro l1; case l1; clear l1; [idtac | intros a1 l1]; (intro l2; case l2; clear l2; [idtac | intros a2 l2]).
Coccinelle/list_extensions/more_list.v:453:intros E a a'; fix 1.
Coccinelle/list_extensions/more_list.v:466:fix 2.
Coccinelle/list_extensions/more_list.v:488:fix 3.
Coccinelle/list_extensions/more_list.v:504:fix 2.
Coccinelle/list_extensions/more_list.v:518:fix 2.
Coccinelle/list_extensions/more_list.v:638:  fix 1.
Coccinelle/list_extensions/more_list.v:668:fix 4.
Coccinelle/list_extensions/more_list.v:693:fix 5.
Coccinelle/list_extensions/more_list.v:708:fix 3.
Coccinelle/list_extensions/more_list.v:743:fix 5.
Coccinelle/list_extensions/more_list.v:760:fix 3.
Coccinelle/list_extensions/more_list.v:777:fix 5.
Coccinelle/list_extensions/more_list.v:829:intros eq_proof RB; fix 2.
Coccinelle/list_extensions/more_list.v:954:intros eq_proof RB; fix 2.
Coccinelle/list_extensions/more_list.v:1006:fix 3.
Coccinelle/list_extensions/more_list.v:1018:fix 3.
Coccinelle/list_extensions/more_list.v:1030:fix 3.
Coccinelle/list_extensions/more_list.v:1044:fix 2.
Coccinelle/list_extensions/more_list.v:1143:fix 3.
Coccinelle/list_extensions/more_list.v:1727:intros A B eq_bool eq_bool_ok P f; fix 1; intro l; case l; clear l; simpl.
Coccinelle/list_extensions/more_list.v:1759:intros A B eq_bool eq_bool_ok P f; fix 1; intro l; case l; clear l; simpl.
Coccinelle/list_extensions/more_list.v:1832:intros A B eq_bool eq_bool_ok P f; fix 1; intro l; case l; clear l.
Coccinelle/list_extensions/more_list.v:1880:intros A B eq_bool eq_bool_ok P f; fix 1; intro l; case l; clear l.
Coccinelle/list_extensions/weaved_relation.v:31:fix 1.
Coccinelle/list_extensions/weaved_relation.v:42:intros A R; fix 1.
Coccinelle/list_extensions/weaved_relation.v:69:fix 3.
Coccinelle/list_extensions/weaved_relation.v:91:fix 4.
Coccinelle/list_extensions/weaved_relation.v:124:fix 3.
Coccinelle/term_algebra/equational_theory.v:1085:    fix 2.
Coccinelle/term_algebra/equational_theory.v:1104:    fix 2.
Coccinelle/term_algebra/equational_theory.v:1141:      fix 5.
Coccinelle/term_algebra/term.v:98:revert l; fix 1.
Coccinelle/term_algebra/term.v:153:fix 1; intros l1 l2; case l1; clear l1.
Coccinelle/term_algebra/term.v:160:fix 1; intro l; case l; clear l.
Coccinelle/term_algebra/term.v:170:fix 1; intro l; case l; clear l.
Coccinelle/term_algebra/term.v:235:revert t1 l; clear f; fix 2.
Coccinelle/term_algebra/term.v:285:fix 1; intros l1 l2; case l1; clear l1.
Coccinelle/term_algebra/term.v:292:fix 1; intro l; case l; clear l.
Coccinelle/term_algebra/term.v:313:fix 2.
Coccinelle/term_algebra/term.v:327:simpl; revert l s_in_l; fix 1.
Coccinelle/term_algebra/term.v:358:fix 1.
Coccinelle/term_algebra/term.v:492:fix 1.
Coccinelle/term_algebra/term.v:713:fix 2.
Coccinelle/term_algebra/term.v:978:fix 1.
Coccinelle/term_algebra/term.v:1010:revert l IH; fix 1.
Coccinelle/term_algebra/term.v:1161:fix 4.
Coccinelle/term_algebra/term.v:1244:fix 2; intros t p; case p; clear p.
Coccinelle/term_algebra/term.v:1537:fix 1.
Coccinelle/term_algebra/term.v:1658:fix 2.
Coccinelle/term_algebra/term.v:1679:fix 2.
Coccinelle/term_algebra/term.v:1698:fix 2.
Coccinelle/term_algebra/term.v:1715:fix 2; intros vars sigma; case sigma; clear sigma.
Coccinelle/term_orderings/interp.v:81:     fix 1.
Coccinelle/term_orderings/interp.v:151:     fix 1.
Coccinelle/term_orderings/interp.v:280:     fix 1.
Coccinelle/term_orderings/isubterm_dp.v:139:revert p k; fix 1.
Coccinelle/term_orderings/matrix.v:137:    fix 1;intros [|dim].
Coccinelle/term_orderings/matrix.v:169:    fix 1.
Coccinelle/term_orderings/matrix.v:243:    fix 1.
Coccinelle/term_orderings/matrix.v:275:    fix 1.
Coccinelle/term_orderings/matrix.v:293:    fix 1.
Coccinelle/term_orderings/matrix.v:312:    fix 1.
Coccinelle/term_orderings/matrix.v:345:    fix 1.
Coccinelle/term_orderings/matrix.v:363:    fix 1.
Coccinelle/term_orderings/matrix.v:381:    fix 1.
Coccinelle/term_orderings/matrix.v:399:    fix 1.
Coccinelle/term_orderings/matrix.v:424:    fix 1.
Coccinelle/term_orderings/matrix.v:454:    fix 1.
Coccinelle/term_orderings/matrix.v:478:    fix 1.
Coccinelle/term_orderings/matrix.v:499:    fix 1.
Coccinelle/term_orderings/matrix.v:530:    fix 1.
Coccinelle/term_orderings/matrix.v:585:    fix 1;intros [|dim].
Coccinelle/term_orderings/matrix.v:615:    revert dim. fix 1.
Coccinelle/term_orderings/matrix.v:698:    fix 1.
Coccinelle/term_orderings/matrix.v:732:    fix 1.
Coccinelle/term_orderings/matrix.v:753:    fix 1.
Coccinelle/term_orderings/matrix.v:774:    fix 1.
Coccinelle/term_orderings/matrix.v:814:    fix 1.
Coccinelle/term_orderings/matrix.v:834:    fix 1.
Coccinelle/term_orderings/matrix.v:854:    fix 1.
Coccinelle/term_orderings/matrix.v:874:    fix 1.
Coccinelle/term_orderings/matrix.v:899:    fix 1.
Coccinelle/term_orderings/matrix.v:934:    fix 1.
Coccinelle/term_orderings/matrix.v:961:    fix 1.
Coccinelle/term_orderings/matrix.v:987:    fix 1.
Coccinelle/term_orderings/matrix.v:1008:    fix 1.
Coccinelle/term_orderings/matrix.v:1028:    fix 1.
Coccinelle/term_orderings/matrix.v:1063:    fix 1.
Coccinelle/term_orderings/matrix.v:1095:    fix 1.
Coccinelle/term_orderings/matrix.v:1122:    fix 1.
Coccinelle/term_orderings/matrix.v:1155:    fix 1.
Coccinelle/term_orderings/matrix.v:1184:    fix 1.
Coccinelle/term_orderings/matrix.v:1219:    fix 1.
Coccinelle/term_orderings/matrix.v:1246:    fix 1.
Coccinelle/term_orderings/matrix.v:1271:    fix 1.
Coccinelle/term_orderings/matrix.v:1300:    fix 1.
Coccinelle/term_orderings/matrix.v:1330:    fix 1.
Coccinelle/term_orderings/matrix.v:1371:    fix 1.
Coccinelle/term_orderings/matrix.v:1404:    fix 1.
Coccinelle/term_orderings/matrix.v:1443:    fix 1.
Coccinelle/term_orderings/matrix.v:1494:    fix 1.
Coccinelle/term_orderings/matrix.v:1541:    fix 1.
Coccinelle/term_orderings/matrix.v:1578:    fix 1.
Coccinelle/term_orderings/matrix.v:1615:    fix 1.
Coccinelle/term_orderings/matrix.v:1681:  fix 1;intros [|dim].
Coccinelle/term_orderings/matrix.v:1695:  fix 1;intros [|dim].
Coccinelle/term_orderings/matrix.v:1736:  fix 1.
Coccinelle/term_orderings/matrix.v:1755:  fix 1;intros [|dim].
Coccinelle/term_orderings/matrix.v:2709:    fix 1.
Coccinelle/term_orderings/matrix.v:2830:    fix 1;intros [|dim].
Coccinelle/term_orderings/matrix.v:2840:    fix 1;intros [|dim].
Coccinelle/term_orderings/matrix.v:2996:    fix 1;intros [|dim].
Coccinelle/term_orderings/matrix.v:3008:    fix 1;intros [|dim].
Coccinelle/term_orderings/rpo.v:562:clear f f_stat prec_eq_f_g; revert l1 l2 L E; fix 1; intro l1; case l1; clear l1.
Coccinelle/term_orderings/subterm_dp.v:138:revert p k; fix 1.
Coccinelle/term_orderings/term_o.v:238:fix 1; intro l1; case l1; clear l1; [idtac | intros a1 l1].
Coccinelle/term_orderings/term_o.v:266:fix 1; intro l; case l; clear l.
Coccinelle/term_orderings/term_o.v:311:fix 1; intro l1; case l1; clear l1.
Coccinelle/unification/free_unif.v:773:fix 1.
Coccinelle/unification/free_unif.v:824:clear p1_diff_q1; revert p1 q1 p1_le_q1 Abs ; fix 1. 
Coccinelle/unification/free_unif.v:848:revert p1 q1 p1_le_q1 p1_diff_q1 ; fix 1. 
Coccinelle/unification/free_unif.v:1503:generalize (VSet.support (domain_of_subst sigma)); fix 1.

Build problem with Coq 8.8

#=== ERROR while installing coq-color.1.4.0 ===================================#
# opam-version 1.2.2
# os           linux
# command      make -j4
# path         /home/vadim/.opam/4.06.1/build/coq-color.1.4.0
# compiler     4.06.1
# exit-code    2
# env-file     /home/vadim/.opam/4.06.1/build/coq-color.1.4.0/coq-color-25182-58c514.env
# stdout-file  /home/vadim/.opam/4.06.1/build/coq-color.1.4.0/coq-color-25182-58c514.out
# stderr-file  /home/vadim/.opam/4.06.1/build/coq-color.1.4.0/coq-color-25182-58c514.err
### stdout ###
# [...]
# COQC Util/FGraph/TransClos.v
# COQC Util/Relation/RedLength.v
# COQC Util/Set/InfSet.v
# COQC Term/WithArity/ARelation.v
# COQC Util/Vector/VecOrd.v
# COQC Term/String/Srs.v
# Makefile.coq:656: recipe for target 'Term/String/Srs.vo' failed
# Makefile.coq:317: recipe for target 'all' failed
# make[1]: Leaving directory '/home/vadim/.opam/4.06.1/build/coq-color.1.4.0'
# Makefile:17: recipe for target 'default' failed
### stderr ###
# Error: Cannot guess decreasing argument of fix.
# [...]
# make[2]: *** [Term/String/Srs.vo] Error 1
# make[2]: *** Waiting for unfinished jobs....
# File "./Util/Vector/VecOrd.v", line 195, characters 2-31:
# Warning: Use of “Require” inside a section is deprecated.
# [require-in-section,deprecated]
# File "./Util/FGraph/TransClos.v", line 305, characters 2-18:
# Warning: Notation _ [=] _ was already used. [notation-overridden,parsing]
# make[1]: *** [all] Error 2
# make: *** [default] Error 2

opam v2. sandboxing

Current package install procedure is incompatible with opam2 sandboxing and it could not be installed unless sandboxing is disabled:

# path        ~/.opam/4.07.0/.opam-switch/build/coq-color.1.5.0                              
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -f Makefile.coq install          
# exit-code   2
# env-file    ~/.opam/log/coq-color-62270-a71bb4.env                                         
# output-file ~/.opam/log/coq-color-62270-a71bb4.out                                         
### output ###
# [...]
# install: mkdir /Users/lord/.opam/4.07.0/lib/coq/user-contrib/CoLoR: Operation not permitted
# install: mkdir /Users/lord/.opam/4.07.0/lib/coq/user-contrib/CoLoR: Operation not permitted

I think the problem is that it attempts to create destination directory, while under sandboxing this directory is already created and the sandbox extends to its content only.

CoLoR cannot be minimized by the bug minimizer due to folder `Set`

I tried to have the bug minimizer minimize ci-color at coq/coq#14722 (comment). It failed to fully minimize because there is a directory named Set/ even though Module Set. is not valid in Coq. Would it be possible to rename the directory Util/Set into something that is a valid module name?

Coq 8.8 support

The coq-released OPAM repository contains the version of coq-color incompatible with the latest Coq release (Coq-8.8):

$ opam install coq-color
The following dependencies couldn't be met:
  - coq-color -> coq-bignums < 8.8~

Please make your project compile with -w "+compatibility-notation"

Please make your project compile with -w "+compatibility-notation" to prepare for the Coq 8.9 release. We would appreciate if this could be done ASAP. If you have trouble doing so, please raise your concern at coq/coq#8383.

Vbuild_spec_obligation_5

I am porting some old proofs for 8.9 to 8.10.2 and immediately stumbled upon a problem. Consider this lemma:

Require Import CoLoR.Util.Vector.VecUtil.
Import VectorNotations.
Open Scope vector_scope.
Lemma Vbuild_1 B gen:
  @Vbuild B 1 gen = [gen 0 (Arith.Lt.lt_0_Sn 0)].
Proof.
  unfold Vbuild.
  cbn.
  apply Vcons_eq.
  split.
  - apply f_equal, Peano_dec.le_unique.
  - reflexivity.
Qed.

After cbn step in Coq-8.9 the goal looks like:

[gen 0 (VecUtil.Vbuild_spec_obligation_4 gen eq_refl)] = [gen 0 (PeanoNat.Nat.lt_0_succ 0)]

However, with Coq 8.10.2 I get:

eq_rect 1 (fun H : nat => vector B H)
[gen 0 (VecUtil.Vbuild_spec_obligation_4 eq_refl)] 1
(VecUtil.Vbuild_spec_obligation_5 eq_refl) = [gen 0 (PeanoNat.Nat.lt_0_succ 0)]

The problem traced back (with help from @zoickx) to the following changeset:

https://github.com/fblanqui/color/compare/f7a4c8a444c54e220c3055a4f4c68a1f214f0a4b..44b6693d71f8ac72b2610f46d97b3c766ffddea5?diff=unified#diff-3802eaffee5b7512dcba958bc4eea1e4

It looks like the following workaround helps:

Lemma Vbuild_1 B gen:
  @Vbuild B 1 gen = [gen 0 (Arith.Lt.lt_0_Sn 0)].
Proof.
  unfold Vbuild.
  cbn.

  assert (h : VecUtil.Vbuild_spec_obligation_5 (eq_refl 1) = eq_refl 1).
  apply eq_unique.
  rewrite h. cbn.

  apply Vcons_eq.
  split.
  - apply f_equal, Peano_dec.le_unique.
  - reflexivity.
Qed.

But it is frankly a bit ugly. Specifically, because it depends on the auto-generated lemma name.
In my project, I use Vbuild a lot and this workaround have to be used a lot. Perhaps there is a better way?

new release for Coq-8.9

Current OPAM release is coq-color-1.5.0 which does not work with Coq-8.9. It is not just OPAM package version check. The source code in release tarball does not compile with Coq-8.9.

However, the current state of this git repository compiles under Coq-8.9 without any changes.

It would be great to make a new release based on the current git master and push it into OPAM. My project depends on coq-color and I could not upgrade to Coq-8.9 because of this problem. I will be glad to help with the release if needed.

coq-8.12 support

The current OPAM version (1.7.0) of coq-color does not support Coq-8.12.
Please consider adding support for 8.12. Thanks!

Recommend Projects

React

A declarative, efficient, and flexible JavaScript library for building user interfaces.
Vue.js

🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
TensorFlow

An Open Source Machine Learning Framework for Everyone
Django

The Web framework for perfectionists with deadlines.
Laravel

A PHP framework for web artisans
D3

Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

javascript

JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
web

Some thing interesting about web. New door for the world.
server

A server is a program made to process requests and deliver data to clients.
Machine learning

Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Visualization

Some thing interesting about visualization, use data art
Game

Some thing interesting about game, make everyone happy.

Recommend Org

Facebook

We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft

Open source projects and samples from Microsoft.
Google

Google ❤️ Open Source for everyone.
Alibaba

Alibaba Open Source for everyone
D3

Data-Driven Documents codes.
Tencent

China tencent open source team.