ejgallego/coq-serapi issues and pull requests

#208 - !pinned flag should not be used in opam package for releases

Issue - State: closed - Opened by palmskog over 4 years ago - 2 comments
Labels: kind: infrastructure

#102 - [sercomp] Disable kernel safety check when in --quick mode.

Pull Request - State: closed - Opened by ejgallego almost 6 years ago - 2 comments
Labels: kind: upstream

#101 - [test] Add two failing tests for --quick

Pull Request - State: closed - Opened by palmskog almost 6 years ago - 7 comments
Labels: kind: bug, kind: testing

#100 - [doc] Add man pages with examples for sercomp and compser

Pull Request - State: closed - Opened by palmskog almost 6 years ago - 2 comments
Labels: kind: documentation

#99 - [sercomp] Add --async-workers option to set max parallel jobs

Pull Request - State: closed - Opened by palmskog almost 6 years ago
Labels: kind: enhancement, part: async

#98 - [sercomp] Improve error exit codes and display.

Issue - State: closed - Opened by ejgallego almost 6 years ago - 3 comments
Labels: kind: documentation

#97 - [ci] Updates to Travis.

Pull Request - State: closed - Opened by ejgallego almost 6 years ago
Labels: kind: infrastructure

#96 - [sercomp] Add experimental `--quick` option to skip proofs.

Pull Request - State: closed - Opened by ejgallego almost 6 years ago - 2 comments
Labels: kind: enhancement, kind: upstream

#95 - [sercomp] Add check mode for compser

Pull Request - State: closed - Opened by palmskog almost 6 years ago - 3 comments
Labels: kind: enhancement

#94 - [test] Add test case showing discrepancy between coqc and sercomp/compser

Pull Request - State: closed - Opened by palmskog almost 6 years ago - 5 comments
Labels: kind: bug, kind: testing

#93 - [test] Add test for setoid_rewrite tactic

Pull Request - State: closed - Opened by palmskog almost 6 years ago - 5 comments
Labels: kind: bug, kind: testing

#92 - [test] Tests for most common ssr serialization errors

Pull Request - State: closed - Opened by palmskog almost 6 years ago - 2 comments
Labels: kind: upstream, kind: testing

#91 - Failing compilation when installing Coq 8.9 from OPAM

Issue - State: closed - Opened by palmskog almost 6 years ago - 15 comments
Labels: kind: upstream

#90 - [test] Add test for abstract tactic

Pull Request - State: closed - Opened by palmskog almost 6 years ago - 6 comments
Labels: kind: bug, kind: upstream, kind: testing

#89 - [test] Add test for functional induction tactic

Pull Request - State: closed - Opened by palmskog almost 6 years ago
Labels: kind: bug, kind: testing

#88 - [test] Add test for instantiate tactic

Pull Request - State: closed - Opened by palmskog almost 6 years ago - 5 comments
Labels: kind: bug, kind: testing

#87 - [sertop] Add `--mode=vo` option that will output a `.vo` file.

Pull Request - State: closed - Opened by ejgallego almost 6 years ago - 4 comments
Labels: kind: enhancement

#86 - [serapi] Add `Assumptions` query.

Pull Request - State: closed - Opened by ejgallego almost 6 years ago - 2 comments
Labels: kind: enhancement, protocol

#85 - [sertop] Set Coq module name correctly from module file.

Pull Request - State: closed - Opened by ejgallego almost 6 years ago - 2 comments
Labels: kind: testing

#84 - [upstream] Problem with deserialization of tactic notations.

Issue - State: closed - Opened by ejgallego almost 6 years ago - 14 comments
Labels: kind: bug, kind: upstream

#83 - [serlib] compser tool with failed deserialization example

Pull Request - State: closed - Opened by palmskog almost 6 years ago - 1 comment
Labels: kind: bug, kind: enhancement

#81 - [test] add test for intropatterns

Pull Request - State: closed - Opened by palmskog almost 6 years ago - 4 comments
Labels: kind: bug

#80 - [serlib] test for Add Field

Pull Request - State: closed - Opened by palmskog almost 6 years ago - 2 comments
Labels: kind: bug

#79 - [serlib] add test for Hint Rewrite

Pull Request - State: closed - Opened by palmskog almost 6 years ago - 2 comments
Labels: kind: bug

#78 - [sercomp] Add option controlling output mode.

Pull Request - State: closed - Opened by ejgallego almost 6 years ago - 4 comments
Labels: kind: enhancement

#77 - [serlib] Functional induction in test

Pull Request - State: closed - Opened by palmskog almost 6 years ago - 2 comments
Labels: kind: bug

#76 - Including modified sercomp and compser programs for testing

Issue - State: closed - Opened by palmskog almost 6 years ago - 12 comments
Labels: kind: enhancement

#75 - Test for Functional Scheme and rename tactic

Pull Request - State: closed - Opened by palmskog almost 6 years ago - 1 comment

#74 - [serlib] add test for fix tactic

Pull Request - State: closed - Opened by palmskog almost 6 years ago - 6 comments
Labels: kind: bug

#73 - [serlib] Fix ssr serialization test (cc #68)

Pull Request - State: closed - Opened by ejgallego almost 6 years ago - 8 comments
Labels: kind: enhancement, kind: upstream

#72 - Create CODE_OF_CONDUCT.md

Pull Request - State: closed - Opened by ejgallego almost 6 years ago
Labels: kind: documentation

#71 - [build] Build SerAPI with Dune.

Pull Request - State: closed - Opened by ejgallego about 6 years ago
Labels: kind: enhancement

#70 - [serlib] Properly handle opaque types non-serialization (fixes #61)

Pull Request - State: closed - Opened by ejgallego about 6 years ago - 6 comments
Labels: kind: enhancement

#69 - [serapi] Add document creation `NewDoc` protocol call.

Pull Request - State: closed - Opened by ejgallego about 6 years ago - 1 comment
Labels: kind: enhancement

#68 - Tactic expression serialization failures

Issue - State: closed - Opened by palmskog about 6 years ago - 16 comments
Labels: kind: bug, kind: upstream

#67 - [serlib] Add serializers for `constr_with_bindings` genarg.

Pull Request - State: closed - Opened by ejgallego about 6 years ago

#66 - Tactic call becomes sexp with "[XXX ser_gen]"

Issue - State: closed - Opened by palmskog about 6 years ago - 6 comments

#65 - [travis] Update to OPAM 2.0, reenable OPAM testing.

Pull Request - State: closed - Opened by ejgallego about 6 years ago
Labels: kind: enhancement

#64 - Invalid characters when feeding back sexps into Coq

Issue - State: closed - Opened by palmskog about 6 years ago - 10 comments
Labels: kind: bug, kind: upstream

#63 - How do I get rid of Warning 58?

Issue - State: closed - Opened by anton-trunov about 6 years ago - 3 comments

#62 - Minor fixes in docs

Pull Request - State: closed - Opened by anton-trunov about 6 years ago - 3 comments
Labels: kind: documentation

#61 - Replace `Obj.magic` in deserialization of abstract datatypes by a more user-friendly error.

Issue - State: closed - Opened by ejgallego about 6 years ago

#60 - sertop "crashes" after a query

Issue - State: closed - Opened by anton-trunov about 6 years ago - 4 comments
Labels: kind: bug

#59 - adding support for reals

Issue - State: closed - Opened by corneliuhoffman about 6 years ago
Labels: kind: enhancement, wontfix, in-progress, fixed by: flèche

#58 - How do I setup OPAM installed sertop.el?

Issue - State: closed - Opened by anton-trunov about 6 years ago - 11 comments
Labels: kind: bug

#57 - `make sercomp` fails on my system

Issue - State: closed - Opened by Ptival about 6 years ago - 1 comment

#56 - Error When Adding a Vernac Command

Issue - State: closed - Opened by yangky11 about 6 years ago - 3 comments
Labels: kind: bug, kind: documentation

#55 - REPL Gets Stuck With Long Inputs

Issue - State: closed - Opened by yangky11 about 6 years ago - 2 comments

#54 - exposing -I in sertop, fixes #53

Pull Request - State: closed - Opened by Ptival about 6 years ago - 6 comments
Labels: kind: enhancement

#53 - Why is `-I` not exposed by sertop?

Issue - State: closed - Opened by Ptival about 6 years ago - 1 comment

#51 - [sertop] Message output from Add delayed to next Query

Issue - State: closed - Opened by riswords over 6 years ago - 5 comments
Labels: kind: documentation

#50 - Support for Kythe?

Issue - State: closed - Opened by ejgallego over 6 years ago - 1 comment
Labels: kind: enhancement, wontfix

#49 - [serapi] Add `Init` call to the protocol.

Issue - State: closed - Opened by ejgallego over 6 years ago - 1 comment
Labels: kind: enhancement, protocol, fixed by: flèche

#48 - Python interface

Issue - State: closed - Opened by ejgallego over 6 years ago - 19 comments
Labels: kind: enhancement, help wanted

#47 - SerAPI unable to respond when handling compcert.cparser.Parser

Issue - State: closed - Opened by jimyu94 over 6 years ago - 3 comments
Labels: to investigate

#46 - Unclear how to use SerAPI demo

Issue - State: closed - Opened by joelburget over 6 years ago - 3 comments
Labels: kind: documentation

#45 - Load packages in parallel.

Pull Request - State: closed - Opened by joelburget over 6 years ago - 4 comments

#44 - Documents on error handling in SerAPI?

Issue - State: closed - Opened by jimyu94 over 6 years ago - 1 comment
Labels: question, kind: documentation

#43 - Expose the tokenizer of Coq?

Issue - State: closed - Opened by jimyu94 over 6 years ago - 1 comment
Labels: kind: enhancement, in-progress

#42 - A likely linking problem

Issue - State: closed - Opened by jimyu94 almost 7 years ago - 2 comments
Labels: kind: bug

#41 - Deserialization of Coq's "generic arguments" is not supported.

Issue - State: closed - Opened by riswords almost 7 years ago - 9 comments
Labels: kind: bug, in-progress

#40 - Fix reference to file that was moved in c9e2bc1.

Pull Request - State: closed - Opened by Zimmi48 about 7 years ago - 1 comment

#39 - v8.7 branch broken with tip of Coq v8.7 branch

Issue - State: closed - Opened by Zimmi48 about 7 years ago - 5 comments
Labels: sexplib

#38 - Line length limitations in sertop

Issue - State: closed - Opened by riswords about 7 years ago - 4 comments
Labels: invalid, kind: documentation

#37 - Build broken by recent change in Coq master

Issue - State: closed - Opened by tchajed over 7 years ago - 3 comments
Labels: kind: bug, in-progress

#36 - Add OPAM file

Issue - State: closed - Opened by corwin-of-amber over 7 years ago - 5 comments

#35 - Pass arguments from _CoqProject file to coqtop

Issue - State: closed - Opened by psteckler over 7 years ago - 14 comments
Labels: kind: enhancement, wontfix

#34 - Changes to sexplib break SerAPI build

Issue - State: closed - Opened by psteckler over 7 years ago - 7 comments

#33 - coqc / coqtop compatibility

Issue - State: closed - Opened by ejgallego over 7 years ago

#32 - Sercomp benchmarking mode.

Issue - State: closed - Opened by ejgallego over 7 years ago
Labels: fixed by: flèche

#31 - Coquille support

Issue - State: closed - Opened by ejgallego almost 8 years ago - 1 comment

#30 - Add Coq8.6 link

Pull Request - State: closed - Opened by zjhmale almost 8 years ago - 4 comments

#29 - Unbound module Feedback

Issue - State: closed - Opened by zjhmale almost 8 years ago - 7 comments

#28 - Query Coq location from environment

Pull Request - State: closed - Opened by zjhmale almost 8 years ago - 3 comments

#27 - No LICENSE info

Issue - State: closed - Opened by Zimmi48 about 8 years ago - 1 comment

#26 - Language Server Protocol

Issue - State: closed - Opened by ejgallego about 8 years ago - 13 comments
Labels: kind: enhancement, fixed by: flèche

#25 - Warn when the Coq location is bogus

Issue - State: closed - Opened by Ptival about 8 years ago - 2 comments

#24 - Some Feedback Message Errors mention a fresh state id

Issue - State: closed - Opened by Ptival over 8 years ago - 8 comments
Labels: kind: upstream, fixed by: flèche

#23 - Elusive error location

Issue - State: closed - Opened by Ptival over 8 years ago - 2 comments
Labels: kind: bug

#22 - Commas in s-expressions: string or unquote?

Issue - State: closed - Opened by Ptival over 8 years ago - 26 comments
Labels: protocol, sexplib, kind: documentation

#21 - Workaround position reporting for UTF-8 scripts

Issue - State: closed - Opened by ejgallego over 8 years ago - 14 comments
Labels: kind: enhancement, protocol, sexplib, fixed by: flèche

#20 - Evar support

Issue - State: closed - Opened by ejgallego over 8 years ago

#19 - Define command line options

Issue - State: closed - Opened by ejgallego over 8 years ago
Labels: kind: enhancement, help wanted

#18 - Javascript Target

Issue - State: closed - Opened by ejgallego over 8 years ago - 4 comments
Labels: wontfix, in-progress, fixed by: flèche

#17 - ZeroMQ support -- Jupyter kernel

Issue - State: closed - Opened by ejgallego over 8 years ago - 16 comments
Labels: kind: enhancement, wontfix, protocol, in-progress

#16 - Clarifing Add and parsing

Issue - State: closed - Opened by gares over 8 years ago - 3 comments
Labels: question, kind: upstream

#15 - Allow `Query` to take a `stateid`

Issue - State: closed - Opened by ejgallego over 8 years ago - 11 comments
Labels: kind: enhancement, protocol

#14 - State id to `Add` the first sentence to

Issue - State: closed - Opened by cpitclaudel over 8 years ago - 26 comments
Labels: protocol, in-progress, kind: documentation

#13 - Enable Async support in SerAPI.

Issue - State: closed - Opened by ejgallego over 8 years ago - 32 comments
Labels: kind: enhancement, help wanted, protocol, kind: upstream, in-progress, fixed by: flèche

#12 - Add feedback filters [Was `.glob` support?]

Issue - State: closed - Opened by ejgallego over 8 years ago - 4 comments
Labels: kind: enhancement, in-progress

#11 - How does EditAt work? / EditAt limitations

Issue - State: closed - Opened by cpitclaudel over 8 years ago - 41 comments
Labels: question, protocol, kind: upstream, in-progress, kind: documentation

#10 - What is the new argument to StmAdd?

Issue - State: closed - Opened by cpitclaudel over 8 years ago - 4 comments
Labels: question

#9 - Some questions wrt porting Proof General to SerAPI

Issue - State: closed - Opened by cpitclaudel over 8 years ago - 2 comments
Labels: question

#8 - `nil` vs `()`

Issue - State: closed - Opened by cpitclaudel over 8 years ago - 4 comments
Labels: sexplib

#7 - Document how to interrupt busy SerAPI.

Issue - State: closed - Opened by cpitclaudel over 8 years ago - 15 comments

#6 - Compilation fail with error 44

Issue - State: closed - Opened by cpitclaudel over 8 years ago - 2 comments

#5 - Support for Whole Document Parsing

Issue - State: closed - Opened by ejgallego over 8 years ago - 11 comments
Labels: kind: upstream, in-progress

#4 - Spurious completion message when exiting

Issue - State: closed - Opened by cpitclaudel over 8 years ago - 2 comments

#3 - Strings versus symbols

Issue - State: closed - Opened by cpitclaudel over 8 years ago - 3 comments
Labels: help wanted, sexplib

#2 - Define protocol and batching options for control commands [Was: Question about Acks]

Issue - State: closed - Opened by cpitclaudel over 8 years ago - 10 comments
Labels: question, protocol, moreinfo

GitHub / ejgallego/coq-serapi issues and pull requests