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

Evar support #20

Closed
ejgallego opened this issue Jul 11, 2016 · 0 comments · May be fixed by #256
Closed

Evar support #20

ejgallego opened this issue Jul 11, 2016 · 0 comments · May be fixed by #256

Comments

@ejgallego
Copy link
Collaborator

We'd like to add support for evar querying.

The XML protocol already provides some support, see
https://github.com/coq/coq/blob/trunk/ide/ide_slave.ml#L223

Also, https://coq.inria.fr/bugs/show_bug.cgi?id=4504 seems very relevant.
@ejgallego ejgallego added this to the 0.7.0 milestone May 18, 2019
@ejgallego ejgallego modified the milestones: 0.7.0, 0.8.0 Oct 25, 2019
@ejgallego ejgallego modified the milestones: 0.11.0, 0.11.1 May 13, 2020
@ejgallego ejgallego modified the milestones: 0.11.1, 0.12.1 May 27, 2020
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)
@ejgallego ejgallego modified the milestones: 0.12.1, 0.13.1 Mar 12, 2021
@ejgallego ejgallego mentioned this issue Sep 21, 2021
Open
ejgallego added a commit that referenced this issue Sep 21, 2021
@ejgallego
[serapi] Support for low-level evar information.
6493ade 
Fixes #20

This is still experimental, in particular we should maybe provide a
better support for handling #251.
@ejgallego ejgallego mentioned this issue Sep 21, 2021
Draft
@ejgallego ejgallego modified the milestones: 0.13.1, 0.16.0 Jun 15, 2022
@ejgallego ejgallego removed this from the 0.16.0 milestone Sep 8, 2022
@ejgallego ejgallego closed this as not planned Won't fix, can't repro, duplicate, stale Feb 15, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

[serapi] Support for low-level evar information. rocq-archive/coq-serapi
1 participant
@ejgallego