Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Support for -indices-matter #222

Closed
cpitclaudel opened this issue Aug 5, 2020 · 1 comment · Fixed by ocaml/opam-repository#17070
Closed

Support for -indices-matter #222

cpitclaudel opened this issue Aug 5, 2020 · 1 comment · Fixed by ocaml/opam-repository#17070
Assignees
@ejgallego
Labels
kind: bug kind: enhancement
Milestone
0.11.1

Comments

@cpitclaudel
Copy link
Collaborator

Coqc and coqtop support -indices-matter; it's needed by HoTT. Is there a way to use it with SerAPI? If not, it would be nice to add it.
@ejgallego ejgallego added this to the 0.12.0 milestone Aug 26, 2020
@ejgallego
Copy link
Collaborator

Indeed the initialization is quite messy, hopefully I can push a refactor to Coq itself so this kind of code is better shared.

@ejgallego ejgallego self-assigned this Aug 26, 2020
@ejgallego ejgallego mentioned this issue Aug 26, 2020
Closed
@ejgallego ejgallego modified the milestones: 0.12.0, 0.11.1 Aug 26, 2020
ejgallego added a commit that referenced this issue Aug 26, 2020
@ejgallego
[sertop] Fix #222 "Support --indices-matter"
a705b25
ejgallego added a commit that referenced this issue Aug 26, 2020
@ejgallego
Merge pull request #223 from ejgallego/v8.11+indices_matter
750dd3e 
[sertop] Fix #222 "Support --indices-matter"
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Aug 26, 2020
@ejgallego
[new release] coq-serapi (8.11.0+0.11.1)
b688d42 
CHANGES:

* [general] Require dune >= 2.0 (@ejgallego, ??)
 * [serapi]  New query `Comments` to return all comments in a document
             (@ejgallego, rocq-archive/coq-serapi#20? , (partially) fixes rocq-archive/coq-serapi#191 , ejgallego/coq-serapi#200 )
 * [general] Coq's error recovery is now disabled by default
             (@ejgallego , fixes rocq-archive/coq-serapi#201)
 * [general] New option `--error-recovery` to enable error recovery
             (@ejgallego , rocq-archive/coq-serapi#203)
 * [general] Bump sexplib dependency to v0.13 (@ejgallego , rocq-archive/coq-serapi#204)
             Fixes incorrect change in rocq-archive/coq-serapi#194.
 * [sertop]  Set default value of allow-sprop to be true in agreement with upstream coq v8.11
             and added option '--disallow-sprop' to optionally switch it off
			 (--disallow-sprop forbids using the proof irrelevant SProp sort)
             (rocq-archive/coq-serapi#199, @pestun)
 * [sertop]  Set default value of allow-sprop to be true in agreement with upstream coq v8.11
             and added option '--disallow-sprop' to optionally switch it off
			 (--disallow-sprop forbids using the proof irrelevant SProp sort)
             (@pestun , rocq-archive/coq-serapi#199)
 * [sertop]  Added option `--topfile` to `sertop` to set top name from
             a filename (rocq-archive/coq-serapi#197, @pestun)
 * [deps]    Require sexplib >= 0.12 , fixed deprecation warnings
             (rocq-archive/coq-serapi#194, @ejgallego)
 * [general] SerAPI is now tested with OCaml 4.08 and 4.09 (rocq-archive/coq-serapi#195 , @ejgallego)
 * [sertop ] Forward port sername from 0.7.1 (@ejgallego)
 * [serlib ] Fix rocq-archive/coq-serapi#212 "Segfault on universes" (@ejgallego, reported by @cpitclaudel , rocq-archive/coq-serapi#214)
 * [serapi ] Fix rocq-archive/coq-serapi#221 "Support COQPATH" (@ejgallego, reported by @cpitclaudel , rocq-archive/coq-serapi#224)
 * [sertop ] Fix rocq-archive/coq-serapi#222 "Support --indices-matter" (@ejgallego, reported by @cpitclaudel , rocq-archive/coq-serapi#223)
 * [sertop ] Fix "Stack overflow in main loop" (@pestun , rocq-archive/coq-serapi#216)
@ejgallego ejgallego mentioned this issue Aug 26, 2020
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Aug 27, 2020
@ejgallego
[new release] coq-serapi (8.11.0+0.11.1)
cb00c63 
CHANGES:

* [general] Require dune >= 2.0 (@ejgallego, ??)
 * [serapi]  New query `Comments` to return all comments in a document
             (@ejgallego, rocq-archive/coq-serapi#20? , (partially) fixes rocq-archive/coq-serapi#191 , ejgallego/coq-serapi#200 )
 * [general] Coq's error recovery is now disabled by default
             (@ejgallego , fixes rocq-archive/coq-serapi#201)
 * [general] New option `--error-recovery` to enable error recovery
             (@ejgallego , rocq-archive/coq-serapi#203)
 * [general] Bump sexplib dependency to v0.13 (@ejgallego , rocq-archive/coq-serapi#204)
             Fixes incorrect change in rocq-archive/coq-serapi#194.
 * [sertop]  Set default value of allow-sprop to be true in agreement with upstream coq v8.11
             and added option '--disallow-sprop' to optionally switch it off
			 (--disallow-sprop forbids using the proof irrelevant SProp sort)
             (rocq-archive/coq-serapi#199, @pestun)
 * [sertop]  Set default value of allow-sprop to be true in agreement with upstream coq v8.11
             and added option '--disallow-sprop' to optionally switch it off
			 (--disallow-sprop forbids using the proof irrelevant SProp sort)
             (@pestun , rocq-archive/coq-serapi#199)
 * [sertop]  Added option `--topfile` to `sertop` to set top name from
             a filename (rocq-archive/coq-serapi#197, @pestun)
 * [deps]    Require sexplib >= 0.12 , fixed deprecation warnings
             (rocq-archive/coq-serapi#194, @ejgallego)
 * [general] SerAPI is now tested with OCaml 4.08 and 4.09 (rocq-archive/coq-serapi#195 , @ejgallego)
 * [sertop ] Forward port sername from 0.7.1 (@ejgallego)
 * [serlib ] Fix rocq-archive/coq-serapi#212 "Segfault on universes" (@ejgallego, reported by @cpitclaudel , rocq-archive/coq-serapi#214)
 * [serapi ] Fix rocq-archive/coq-serapi#221 "Support COQPATH" (@ejgallego, reported by @cpitclaudel , rocq-archive/coq-serapi#224)
 * [sertop ] Fix rocq-archive/coq-serapi#222 "Support --indices-matter" (@ejgallego, reported by @cpitclaudel , rocq-archive/coq-serapi#223)
 * [sertop ] Fix "Stack overflow in main loop" (@pestun , rocq-archive/coq-serapi#216)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@ejgallego ejgallego

Labels
kind: bug kind: enhancement
Projects
None yet
Milestone
0.11.1
Development

Successfully merging a pull request may close this issue.

[new release] coq-serapi (8.11.0+0.11.1) ejgallego/opam-repository
2 participants
@ejgallego @cpitclaudel