Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • hamelin/jscoq-light
  • rousselin/jscoq-light
2 results
Show changes
Hide whitespace changes
Inline Side-by-side
Showing
with 1344 additions and 89 deletions
package.json.wacoq deleted 100644 → 0
View file @ 76484498
{
"name": "wacoq",
"version": "0.17.0",
"description": "A port of Coq to WebAssembly -- run Coq in your browser",
"type": "module",
"main": "frontend/classic/js/index.js",
"bin": {
"wacoqdoc": "frontend/classic/js/jscoqdoc.js"
},
"dependencies": {
"array-equal": "^1.0.0",
"child-process-promise": "^2.2.1",
"codemirror": "^5.61.0",
"commander": "^5.0.0",
"fflate-unzip": "^0.7.0",
"find": "^0.3.0",
"glob": "^7.1.3",
"jquery": "^3.6.0",
"jszip": "^3.5.0",
"localforage": "^1.7.3",
"lodash": "^4.17.20",
"minimatch": "^3.0.4",
"mkdirp": "^1.0.4",
"neatjson": "^0.8.3",
"path": "^0.12.7",
"proper-lockfile": "^4.1.2",
"vue": "^2.6.12",
"vue-context-menu": "^2.0.6"
},
"devDependencies": {
"@corwin.amber/hastebin": "^0.1.2",
"@types/codemirror": "^5.60.5",
"@types/find": "^0.2.1",
"@types/jquery": "^3.5.14",
"@types/mkdirp": "^1.0.1",
"@types/node": "^13.11.1",
"assert": "^2.0.0",
"bootstrap": "^5.1.3",
"buffer": "^6.0.3",
"constants-browserify": "^1.0.0",
"css-loader": "^5.2.4",
"file-loader": "^6.0.0",
"katex": "^0.15.3",
"mathjax": "^3.2.2",
"mocha": "^9.1.3",
"path-browserify": "^1.0.1",
"process": "^0.11.10",
"ronin-p2p": "^0.1.0",
"sass": "^1.26.3",
"sass-loader": "^8.0.2",
"stream-browserify": "^3.0.0",
"style-loader": "^1.1.3",
"ts-loader": "^9.3.1",
"typescript": "^4.7.4",
"util": "^0.12.4",
"vue-loader": "^15.9.8",
"vue-template-compiler": "^2.6.12",
"webpack": "^5.49.0",
"webpack-cli": "^4.7.2"
},
"files": [
"frontend",
"backend/*.js",
"backend/*.ts",
"examples",
"dist",
"examples",
"docs/*.html",
"jscoq.js",
"index.html"
],
"scripts": {
"build": "webpack --mode production",
"build:dev": "webpack",
"watch": "webpack -w",
"prepack": "sed -i.in 's/\\(is_npm:\\) false/\\1 true/;s/\\(backend:\\) .*/\\1 '\\'wa\\',/ frontend/classic/js/index.js"
},
"repository": {
"type": "git",
"url": "git+https://github.com/jscoq/jscoq.git"
},
"author": "ejgallego",
"license": "AGPL-3.0-or-later",
"bugs": {
"url": "https://github.com/jscoq/jscoq/issues"
},
"homepage": "https://jscoq.github.io"
}
coq-serapi @ 0bd0772f
Compare 0bd0772f...0bd0772f
Subproject commit 0bd0772fe683d1dbfd3bd29db5ad652e74a70f66
vendor/coq-serapi/.github/workflows/ci.yml 0 → 100644
View file @ 2a40a0b1
name: CI
on:
push:
branches:
- v8.8
- v8.9
- v8.10
- v8.11
- v8.12
- v8.13
- v8.14
- v8.15
- v8.16
- v8.17
- main
pull_request:
branches:
- v8.8
- v8.9
- v8.10
- v8.11
- v8.12
- v8.13
- v8.14
- v8.15
- v8.16
- v8.17
- main
# Allows you to run this workflow manually from the Actions tab
workflow_dispatch:
jobs:
build:
strategy:
fail-fast: false
matrix:
ocaml-compiler: [4.09.x, 4.10.x, 4.11.x, 4.12.x, 4.13.x, 4.14.x, 5.0.x]
test-target: [test]
extra-opam: [coq.8.17.dev coq-mathcomp-ssreflect.dev]
include:
- ocaml-compiler: ocaml-variants.4.12.1+options,ocaml-option-32bit
test-target: js-dune
extra-opam: coq.8.17.dev js_of_ocaml js_of_ocaml-lwt zarith_stubs_js
- ocaml-compiler: 4.13.1
test-target: test
extra-opam:
coq-from-git: true
env:
OPAMJOBS: "2"
OPAMROOTISOK: "true"
OPAMYES: "true"
NJOBS: "2"
COQ_REPOS: "https://github.com/coq/coq.git"
COQ_BRANCH: "v8.17"
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2
- name: Install apt dependencies
run: |
sudo dpkg --add-architecture i386
sudo apt-get -o Acquire::Retries=30 update -q
sudo apt-get -o Acquire::Retries=30 install gcc-multilib libgmp-dev:i386 -y --allow-unauthenticated
- name: Set up OCaml ${{ matrix.ocaml-compiler }}
uses: avsm/setup-ocaml@v2
with:
ocaml-compiler: ${{ matrix.ocaml-compiler }}
dune-cache: true
- name: Basic OPAM setup for SerAPI
run: |
eval $(opam env)
opam repos add coq-released http://coq.inria.fr/opam/released
opam repos add coq-core-dev http://coq.inria.fr/opam/core-dev
# Only for mathcomp.dev which is needed for 8.16, remove when math-comp is fixed
opam repos add coq-extra-dev http://coq.inria.fr/opam/extra-dev
# coq-serapi already pinned by the setup-ocaml@v2 action
opam install --deps-only coq-serapi
- name: Display OPAM Setup
run: |
eval $(opam env)
opam list
- name: Install Coq via git
if: ${{ matrix.coq-from-git }}
run: |
eval $(opam env)
opam pin add -k version dune 3.3.1
# First we update SERAPI_COQ_HOME for future steps as per https://docs.github.com/en/actions/reference/workflow-commands-for-github-actions#setting-an-environment-variable
echo "SERAPI_COQ_HOME=$HOME/coq-$COQ_BRANCH/_build/install/default/lib/" >> $GITHUB_ENV
# Update to coq-core some day
# opam install --deps-only coq-core
opam install --deps-only coq-core
git clone --depth=3 -b "$COQ_BRANCH" "$COQ_REPOS" "$HOME/coq-$COQ_BRANCH"
# Upstream 'make -C "$HOME/coq-$COQ_BRANCH" world' target now builds coqide
cd "$HOME/coq-$COQ_BRANCH"
./configure -prefix "$HOME/coq-$COQ_BRANCH/_build/install/default/"
make dunestrap
dune build -p coq-core,coq-stdlib,coq
cd "$HOME"
# Install math-comp using Coq from git
PATH="$HOME/coq-$COQ_BRANCH/_build/install/default/bin:$PATH"
git clone --depth=3 -b master https://github.com/math-comp/math-comp.git
make -C math-comp/mathcomp/ssreflect
make -C math-comp/mathcomp/ssreflect install
- name: Extra OPAM Setup (Coq, js_of_ocaml)
if: ${{ matrix.extra-opam != '' }}
run: |
eval $(opam env)
opam install ${{ matrix.extra-opam }}
- name: Build and Test SerAPI
run: |
eval $(opam env)
make -j "$NJOBS" SERAPI_COQ_HOME="$SERAPI_COQ_HOME" "${{ matrix.test-target }}"
ls -lR _build/install/default/ || true
ls -lR _build/default/sertop/*.js || true
vendor/coq-serapi/.gitignore 0 → 100644
View file @ 2a40a0b1
_build
*~
js/sertop_js.js
sertop/ser_version.ml
.merlin
*.install
vendor/coq-serapi/.ocamlformat 0 → 100644
View file @ 2a40a0b1
sequence-style=terminator
vendor/coq-serapi/AUTHORS 0 → 100644
View file @ 2a40a0b1
Emilio Jesús Gallego Arias
Karl Palmskog
Vasily Pestun
Clément Pit--Claudel
Kaiyu Yang
vendor/coq-serapi/CHANGES.md 0 → 100644
View file @ 2a40a0b1
## Version 0.17.3
- [serlib] Fix (@ejgallego, #398, fixes #397 fixes sr-lab/coqpyt#35 ,
thanks to @laetitia-teo and @Nfsaavedra for the bug
report)
## Version 0.17.2:
- [serlib] Expose some more Ast functions required by coq-lsp's
auto-build support (@ejgallego, #383)
## Version 0.17.1:
- [sertop] Don't initialize `CoqworkmgrApi` (@ejgallego, #340)
- [serlib] Compat with Jane Street libraries >= v0.16.0 (@ejgallego,
#351)
## Version 0.17.0:
- [serlib] (!) Serialization format of generic arguments has changed
to be conforming to usual `ppx_sexp_conv` conventions.
(@ejgallego , fixes #273)
- [serapi] (!) support for Coq 8.17, upstream structures seem pretty
stable from 8.16, except for `Constr.Evar` (@ejgallego)
- [serapi] SerAPI is now in Coq's CI (@ejgallego @alizter)
## Version 0.16.3:
- [serlib] Fix JSON serialization for generic arguments (@ejgallego, #321)
## Version 0.16.2:
- [sertop] Add `--impredicative-set` command line option (@dhilst , #288)
- [serlib] Added support for some more plugins from coq-core (ltac2,
cc, micromega, number_string_notation) (@ejgallego, #284, #306)
## Version 0.16.1:
- [sertop] Allow to set `--coqlib` using the `COQLIB` environment
variable. The cmdline argument option still has
precedence.
- [serapi] Allow to parse expressions too with
`(Parse (entry Constr) $text)` (@ejgallego, fixes #272)
## Version 0.16.0:
- [serapi] (!) support for Coq 8.16, see upstream changes and SerAPI
test-suite changes for more information. Remarkable
changes are:
- kernel terms are serialized a bit differently now due to
KerName being used in more places upstream. Some
internal structures also changes in kernel's env, so be
attentive if you are depending on them.
- plugin loading is adapted for 8.16 findlib loading
method
(@ejgallego)
- [deps] Require cmdliner >= 1.1.0 (@ejgallego)
- [deps] Support Jane Street libraries v0.15.0 (@ejgallego)
- [serapi] New query `Objects` to dump Coq's libobject (@ejgallego)
- [serlib] Much improved yojson / json support (@ejgallego)
- [serlib] Coq AST now supports ppx_hash intf (ignoring locations by default)
(@ejgallego)
- [serlib] Coq AST now supports ppx_compare intf (ignoring locations by default)
(@ejgallego)
- [serlib] Large refactoring on Serlib, using functors, see serlib/README.md
(@ejgallego)
- [serapi] (!) Query `Proofs` has changed type and will now return the
partial terms under construction (#271 , fixes #270, @ejgallego)
## Version 0.15.1:
- [serlib] Fix bad bypass of opaquetab serialization. This caused a
segfault in some cases.
## Version 0.15.0:
- [serapi] (!) support for Coq 8.15, see upstream changes; nothing
too remarkable so far, except for `NewTip` -> `NewAddTip`
in the answer response, we may want to add a compat layer
for this if problematic. (#265, @ejgallego)
## Version 0.14.0:
- [serapi] (!) support for Coq 8.14, see upstream changes; nothing
too remarkable other than `NewDoc` will now ignore
loadpaths due to new init setup upstream.
(#253, @ejgallego)
- [ci] SerAPI branches should be able to build now against Coq rc
packages as to better integrate with Coq's platform beta
release; thanks to Érik Martin-Dorel, Karl Palmskog and Théo
Zimmermann for feedback.
## Version 0.13.1:
- [serapi] New query `(Query () (LogicalPath file))` which will
return the logical path for a particular `.v` file
(@ejgallego, see also
https://github.com/cpitclaudel/alectryon/pull/25)
- [serapi] new `(SaveDoc opts)` command supporting saving of .vo
files even when from interactive mode; note that using
`--topfile` is required (fixes #238, @ejgallego, reported
by Jason Gross)
- [sertop] we don't link the OCaml `num` library anymore, this could
have some impact on plugins (@ejgallego)
- [nix] Added Nix support (#249, fixes #248, @Zimmi48, reported
by @nyraghu)
- [serapi] Fix COQPATH support: interpret paths as absolute (#249, @Zimmi48)
- [serlib] Ignore `env` parameter in certain exceptions (#254, fixes #250,
@ejgallego, reported by @cpitclaudel)
- [sertop] New option `--omit_env` that will disable the serialization of
Coq's super heavy global environments (#254 @ejgallego)
- [build] Test OCaml 4.12 (#257 @ejgallego)
- [sertop] Async mode was not working due to passing `-no-glob` to workers
## Version 0.13.0:
- [serapi] (!) support for Coq 8.13, see upstream changes; in
particular there are changes in the kernel representation
of terms [pattern matching, new caseinvert, primitive arrays]
(#232, fixes #227, @ejgallego)
## Version 0.12.1:
* [serapi] (!) Bump public library versioning [breaking change]
* [opam] Bump upper bound on ppx_sexp_conv to 0.15, allowing SerAPI
to work with the 0.14 set of Jane Street packages.
* [serapi] Fix goal printing anomaly (#230, fixes #228 @corwin-of-amber)
* [sertop ] New `(Fork (fifo_in file) (fifo_out file))` command, that
will (hard) fork a new SerAPI process and redirect the
input / output towards the given Unix FIFOs. This API is
experimental but should allow quite a few advantages to
some users willing to perform speculative execution.
(#210 , improves #202 , @ejgallego)
- [serapi] Fix missing newline to separate goals (#235, fixes #231, @ejgallego)
## Version 0.12.0:
* [general] (!) support Coq 8.12, main changes upstream related to
the representation of numerals and notations.
The rest of the interface does remain relative stable.
(@ejgallego).
## Version 0.11.1:
* [general] Require dune >= 2.0 (@ejgallego, ??)
* [serapi] New query `Comments` to return all comments in a document
(@ejgallego, #20? , (partially) fixes #191 , #200 )
* [general] Coq's error recovery is now disabled by default
(@ejgallego , fixes #201)
* [general] New option `--error-recovery` to enable error recovery
(@ejgallego , #203)
* [general] Bump sexplib dependency to v0.13 (@ejgallego , #204)
Fixes incorrect change in #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)
(#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 , #199)
* [sertop] Added option `--topfile` to `sertop` to set top name from
a filename (#197, @pestun)
* [deps] Require sexplib >= 0.12 , fixed deprecation warnings
(#194, @ejgallego)
* [general] SerAPI is now tested with OCaml 4.08 and 4.09 (#195 , @ejgallego)
* [sertop ] Forward port sername from 0.7.1 (@ejgallego)
* [serlib ] Fix #212 "Segfault on universes" (@ejgallego, reported by @cpitclaudel , #214)
* [serapi ] Fix #221 "Support COQPATH" (@ejgallego, reported by @cpitclaudel , #224)
* [sertop ] Fix #222 "Support --indices-matter" (@ejgallego, reported by @cpitclaudel , #223)
* [sertop ] Fix "Stack overflow in main loop" (@pestun , #216)
## Version 0.11.0:
* [general] (!) support Coq 8.11, a few datatypes have changed, in
particular `CoqAst` handles locations as an AST node, and
the kernel type includes primitive floats (@ejgallego).
* [general] (!) Now the `sertop` and `serapi` OCaml libraries are
built packed, we've also bumped their compat version number
(#192 @ejgallego)
## Version 0.7.1:
* [sertop ] Add `sername` program for batch serialization elaborated terms
Note that this utility will be deprecated in future versions,
to be subsumed by `Query`.
(#207, @palmskog, with help from @ejgallego)
* [serlib ] Expose `QueryUtil.info_of_id` and `gen_pp_obj` in `serapi_protocol.mli` to enable
using them in `sername` to retrieve serialized body-type pairs (@palmskog)
* [general] Improved compat with Jane Street v0.13 toolchain
* [serlib ] Only use `ssreflect` from Coq in tests (@ejgallego)
## Version 0.7.0:
* [general] (!) support Coq 8.10,
* [serapi] (!) `Goals` query return type has been modified due to
upstream changes. (@ejgallego)
* [serlib] Complete (hopefully) serialization for ssreflect ASTs.
(#73 @ejgallego)
* [general] Drop support for OCaml < 4.07 (#140 @ejgallego)
* [serlib ] JSON serialization for kernel and AST terms (@ejgallego)
* [serapi ] Add `Complete` support (@ejgallego
c.f. https://github.com/coq/coq/pull/8766)
* [serlib ] Serlib is now built as a wrapped module (@ejgallego)
* [serapi ] (!) Goals info has been extended to print name metadata if available,
cc #151 (@ejgallego , suggested by @cpitclaudel)
* [serlib ] JSON support for vernac_expr (@ejgallego)
* [sertop ] (!) Do as Coq upstream and load Coq's stdlib with `-R` (closes #56)
* [sertop ] Follow Coq upstream and unset `indices_matter` (closes #157,
thanks to @palmskog for the report)
* [serapi ] (!) Improve CoqExn answer to have pretty-printed message (improves #162,
thanks to @cpitclaudel for the request)
* [serlib ] (!) Fix capitalization conventions for a few types in `Names`
(closes #167 thanks to @corwin-of-amber for the report)
* [serapi ] (!) Add bullet suggest information to goal query (@corwin-of-amber)
* [sertop ] Add `--no_prelude` option (closes #176, @ejgallego, request of @darbyhaller)
* [serlib ] (!) Add index to `MBId` serialization (fixes #150, @ejgallego)
* [serapi ] (!) Add `sid` parameter to `Print` (helps #150, @ejgallego, reported by @cpitclaudel)
* [sertop ] Add `sertok` program for batch serialization of tokens and their source locations (@palmskog)
* [serapi ] (!) Add string-formatted messages to `CoqExn` and `Message`
(@ejgallego closes #184 , closes #162)
## Version 0.6.1:
* [serapi ] Add `Parse` command to parse a sentence; c.f.
https://github.com/ejgallego/coq-serapi/issues/117
(@ejgallego) (cc: @yangky11)
* [sercomp] Add "print" `--mode` to print the input Coq document
(@ejgallego) (cc: @Ptival)
* [serlib ] Serialize `Universe.t` (@ejgallego, request by @yangky11)
* [sercomp] Merge `sercomp` and `compser`, add `--input` parameter to `sercomp`
(@palmskog) (cc: @ejgallego)
* [serlib ] Much improved support for serialization of `Environ.env`
(@yangky11 and @ejgallego c.f. #118)
* [serapi ] Make sure every command ends with `Completed`, even if it produced
an exception (@brando90 and @ejgallego c.f. #124)
* [sercomp] Add `--mode=kexp` to output the final kernel environment.
(@ejgallego c.f. #119)
* [serlib ] Serialize more internal environment fields (@ejgallego c.f. #119)
* [serlib ] Improvements in serialization org (@ejgallego)
* [serlib ] Serialize kernel entries (@ejgallego @palmskog)
* [serlib ] Fix critical bug on `Constr` deserialization; reported by @palmskog,
fix by @SkySkimmer.
* [sertop] Fix backtrace printing when using `--debug` (@ejgallego)
* [serlib ] Don't serialize VM values (@ejgallego, bug report by @palmskog)
* [serapi ] Output location on tokenization (@ejgallego , idea by @palmskog)
* [serapi ] Add basic documentation of the protocol (@ejgallego cc #109)
## Version 0.6.0:
* [general] support Coq 8.9,
* [general] SerAPI now uses Dune as a build system,
* [opam] install `sertop.el`,
* [serlib] support to serialize kernel environments,
* [serapi] new query `Env` that tries to print the current kernel environment,
* [serlib] correct field names for `CAst`,
* [serlib] more robust support for opaque / non-serializable types (#61, #68).
Thanks to @palmskog,
* [serlib] new option `--exn_on_opaque` to raise an exception on
non-serializable types; closes #61, thanks to @palmskog,
* [serlib] serialization test-suite from
https://github.com/proofengineering/serapi-tests, thanks to
@palmskog,
* [sercomp] add `--mode` option to better control output,
* [sercomp] add `compser` for deserialization (inverse of `sercomp`)
(@palmskog),
* [serapi] Allow custom document creation using the `NewDoc` call.
Use the `--no_init` option to avoid automatic creation
on init. (@ejgallego)
* [sercomp] Allow compilers to output `.vo` (@ejgallego , suggested by
@palmskog)
* [sercomp] Serialize top-level vernaculars with their syntactic
attributes (such as location) (@ejgallego)
* [serapi] Add `Assumptions` query, at the suggestion of @Armael
(@ejgallego)
* [sercomp] Disable error resilience mode in compilers; semantics are
a bit dubious see coq/coq#9204 also #94.
(@ejgallego, report by @palmskog)
* [sercomp] Add `check` mode to compilers to check all proofs without
outputting `.vo`. (@palmskog)
* [sercomp] Add "hacky" `--quick` option to skip checking of opaque
proofs. (@ejgallego, request by @palmskog)
* [sercomp] Add `--async_workers` option to set maximum number
of parallel async workers. (@palmskog)
* [sertop] Stop linking Coq plugins statically and load `serlib`
plugins when Coq plugins are loaded instead (@ejgallego,
review by @palmskog)
## Version 0.5.7:
* [serlib] Fixed serializers for more tactics data, add support for
`ground` plugin (#68). Thanks again to @palmskog for the report.
## Version 0.5.6:
* [serlib] Fixed serializers for some tactics data (#66) Thanks to
@palmskog for the report.
## Version 0.5.5:
* [serlib] Be more lenient when parsing back `Id.t` as to accommodate
hacks in the Coq AST (#64) Thanks to @palmskog for the report.
## Version 0.5.4:
* [serlib] Fix critical bug in handling of abstract type (#60)
## Version 0.5.3:
* [sertop] Support for `-I` option (`--ml-include-path`).
## Version 0.5.2:
* [serlib] Compatibility with OCaml 4.07.0 [problems with `Stdlib` packing]
## Version 0.5.1:
* [serlib] (basic) support for serialization of the ssreflect grammar,
* [serapi] `(Query () (Ast n))` is now `(Query ((sid n)) Ast)`,
* [serapi] remove broken deprecated `SetOpt` and `LibAdd` commands,
* [doc] Improved man page.
* [js] Miscellaneous improvements on the js build.
## Version 0.5.0:
* [general] support Coq 8.8, use improved document API,
* [sertop] By default `sertop` will create a new document with `doc_id` 0,
* [sertop] new debug options, see `sertop --help`.
## Version 0.4:
* [general] support Coq 8.7 , make use of improved upstream API,
* [sertop] support `-R` and `-Q` options, note the slightly different
syntax wrt Coq upstream: `-R dir,path` in place of `-R dir path`,
* [serlib] support serialization of generic arguments [#41],
* [serapi] `(ReadFile file)`: hack to load a completed file.
## Version 0.2:
* Better Query/Object system.
## Version 0.1:
* Serialization-independent protocol core,
* [js] Javascript worker,
* [lib] Better Prelude support,
* [serlib] Full Serialization of generic arguments,
* [proto] Add is not a synchronous call anymore,
* [proto] Refactor into a flat command hierarchy,
* [proto] More useful queries,
* [proto] Guarantee initial state is 1,
* [proto] Support for ltac profiling,
* [proto] Printing: add depth limiting,
* [proto] Better handling of options in the sexp backend.
## Version 0.03:
* **[done]** Implicit arguments.
* **[done]** Coq Workers support.
* **[done]** Advanced Sentence splitting `(Parse (Sentence string))`, which can handle the whole document.
## Version 0.02:
* **[done]** Serialization of the `Proof.proof` object.
* **[done]** Improve API: add options.
* **[done]** Improve and review printing workflow.
* **[done]** `(Query ((Prefix "add") (Limit 10) (PpStr)) $ObjectType)`
* **[done]** Basic Sentence splitting `(Parse num string))`, retuns the first num end of the sentences _without_ executing them.
This has pitfalls as parsing is very stateful.
* **[done]** Basic completion-oriented Search support `(Query () Names)`
* **[done]** Better command line parsing (`Cmdliner`, `Core` ?)
* **[partial]** Print Grammar tactic. `(Query ... (Tactics))`.
Still we need to decide on:
`Coq.Init.Notations.instantiate` vs `instantiate`, the issue of
`Nametab.shortest_qualid_of_global` is a very sensible one for IDEs
vendor/coq-serapi/CODE_OF_CONDUCT.md 0 → 100644
View file @ 2a40a0b1
The SerAPI project aims to be a fun and safe space where everybody is
extremely welcome to participate and discuss. There will be zero
tolerance to any kind of inappropriate behavior. Lets us all have fun.
-- EJGA
# Contributor Covenant Code of Conduct
## Our Pledge
In the interest of fostering an open and welcoming environment, we as
contributors and maintainers pledge to making participation in our project and
our community a harassment-free experience for everyone, regardless of age, body
size, disability, ethnicity, sex characteristics, gender identity and expression,
level of experience, education, socio-economic status, nationality, personal
appearance, race, religion, or sexual identity and orientation.
## Our Standards
Examples of behavior that contributes to creating a positive environment
include:
* Using welcoming and inclusive language
* Being respectful of differing viewpoints and experiences
* Gracefully accepting constructive criticism
* Focusing on what is best for the community
* Showing empathy towards other community members
Examples of unacceptable behavior by participants include:
* The use of sexualized language or imagery and unwelcome sexual attention or
advances
* Trolling, insulting/derogatory comments, and personal or political attacks
* Public or private harassment
* Publishing others' private information, such as a physical or electronic
address, without explicit permission
* Other conduct which could reasonably be considered inappropriate in a
professional setting
## Our Responsibilities
Project maintainers are responsible for clarifying the standards of acceptable
behavior and are expected to take appropriate and fair corrective action in
response to any instances of unacceptable behavior.
Project maintainers have the right and responsibility to remove, edit, or
reject comments, commits, code, wiki edits, issues, and other contributions
that are not aligned to this Code of Conduct, or to ban temporarily or
permanently any contributor for other behaviors that they deem inappropriate,
threatening, offensive, or harmful.
## Scope
This Code of Conduct applies both within project spaces and in public spaces
when an individual is representing the project or its community. Examples of
representing a project or community include using an official project e-mail
address, posting via an official social media account, or acting as an appointed
representative at an online or offline event. Representation of a project may be
further defined and clarified by project maintainers.
## Enforcement
Instances of abusive, harassing, or otherwise unacceptable behavior may be
reported by contacting the project team at e@x80.org. All
complaints will be reviewed and investigated and will result in a response that
is deemed necessary and appropriate to the circumstances. The project team is
obligated to maintain confidentiality with regard to the reporter of an incident.
Further details of specific enforcement policies may be posted separately.
Project maintainers who do not follow or enforce the Code of Conduct in good
faith may face temporary or permanent repercussions as determined by other
members of the project's leadership.
## Attribution
This Code of Conduct is adapted from the [Contributor Covenant][homepage], version 1.4,
available at https://www.contributor-covenant.org/version/1/4/code-of-conduct.html
[homepage]: https://www.contributor-covenant.org
For answers to common questions about this code of conduct, see
https://www.contributor-covenant.org/faq
vendor/coq-serapi/CONTRIBUTING.md 0 → 100644
View file @ 2a40a0b1
## Contributing to SerAPI
Thanks for willing to contribute to SerAPI! Contributing is usually as
easy as opening a pull request, issue, or dropping by the Gitter
channel and letting us know what you think of the tool.
Nothing special has to be kept in mind, other than standard OCaml
practice, we usually follow `ocp-indent` guidelines, but we are
liberal in some places in particular with regards to intra-line
indentation.
We prefer GPG signed commits as well as `Signed-off-by` commits.
## Releasing SerAPI
As of today, SerAPI is released using a standard process based on
`dune-release`; to do a release, it should suffice to do:
```
$ dune-release tag $version
$ dune-release
```
where `$version` is `$coq-version+$serapi_version`, for example
`8.16.2+0.16.4`. Note that `dune-release` requires you to setup a
github token, see `dune-release` docs for more details.
**Important**: note that `dune-release` will automatically generate
the changelog from `CHANGES.md`, please keep the formatting tidy in
that file!
Note that bug https://github.com/ejgallego/coq-serapi/issues/208 may
require you to edit the opam-repository PR if their linter fails
[seems fixed as of today, but OMMV]
### Commit tag conventions [work in progress]:
We have somme
- [serlib] : Serialization lib.
- [test] : Adding or modifying a test.
- [sertop] : Sexp Toplevel.
- [doc] : Documentation.
- [build] : Build system.
- [misc] : Code refactoring, miscellanenous
- [proto] : Core protocol.
- [control] : STM protocol.
- [query] : Query protocol.
- [parse] : Parsing protocol.
- [print] : Printing protocol.
- [js] : Javascript version.
vendor/coq-serapi/FAQ.md 0 → 100644
View file @ 2a40a0b1
## What is SerAPI?
Is a library plus a set of command line tools aimed to improve the
communication of third party tools with Coq.
## How mature is SerAPI?
SerAPI has _experimental_ status; while there are no protocol
stability guarantees, we got moderate experience with it and evolution
should be controlled. SerAPI have been used with success in several
research projects. Protocol-breaking changes are marked in the
changelog with `(!)`.
## Which Coq versions does SerAPI support?
At the moment, Coq 8.12 is the current supported version for the
current protocol. Older versions (8.6---8.11) work, however the
protocol and feature sets do differ.
## How can I install SerAPI?
The supported way is to use the OPAM package manager. The
`.travis.yml` file contains up to date install instructions if you
want to build SerAPI manually, see also the [build instructions](notes/build.md) file.
## What serialization formats does SerAPI provide?
SerAPI was built to encode Coq native data types to/from
S-Expressions, a widely used data and code format pioneered by the
lisp programming language.
Since then, SerAPI has evolved to take advantage of other formats, and
now provides experimental Python and JSON output formats too.
## What kind of S-expressions does SerAPI use?
SerAPI does use Jane Street's excellent
[sexplib](https://github.com/janestreet/sexplib) library print and
parse S-exps; note that there is not really a S-exp standard, for more
details about some differences on how quoting happens in `sexplib`,
please see issues https://github.com/ejgallego/coq-serapi/issues/3 ,
https://github.com/ejgallego/coq-serapi/issues/8 , and
https://github.com/ejgallego/coq-serapi/issues/22 .
## SerAPI hangs with inputs larger than 4096 characters:
This is due to a historical limitation of the UNIX/Linux TTY API. See
[#38](https://github.com/ejgallego/coq-serapi/issues/38). If you
communicate with SerAPI using a **pipe** this shouldn't be a problem.
Alternatively, you can use the `ReadFile` experimental command.
## I get an error "Cannot link ml-object ..."
Your OCaml path is not properly setup, see [build instructions](notes/build.md) for more help.
## Can SerAPI produce `.vo` files?
Yes, see `sercomp --help`
## How does SerAPI compare to TCoq
[TCoq](https://github.com/ml4tp/tcoq/) provides some support for
exporting Coq structures; the main differences with SerAPI is that
SerAPI works against stock Coq and is maintained; it also provides a
faithful, automatically generated printers.
A more detailed comparison is needed, in particular TCoq does provide
some hooks that insert themselves in the proof execution, it is not
clear that SerAPI can provide that.
For a more detailed discussion see
https://github.com/ejgallego/coq-serapi/issues/109
## Can SerAPI evaluate a document incrementally?
Yes, by using Coq's capabilities to that effect. Just issue the proper
`(Cancel ...)` `(Add ... ...)` sequence to simulate an update. This is
limited now to prefix-only incremental evaluation. It will be improved
in the future.
## Does SerAPI support asynchronous proof processing?
Yes, it does. Note however that asynchronous proof processing is still
in experimental status upstream. In particular, there are some issues
on Windows, and `EditAt` may be inconvenient to use. We recommend not
using `EditAt` and instead using the less powerful `Cancel` for now.
## Does SerAPI support Coq's command line flags:
We support only a limited set of `coqtop` command line flags, in
particular `-R` and `-Q` for setting library paths. Unfortunately, due
to our command line parsing library, the format is slightly
different. See `sertop --help` for a comprehensive list of flags.
SerAPI aims to be "command line flag free", with all the options for
each document passed in the document creation call, so this will be
the preferred method.
## What does SerAPI expose?
SerAPI exposes all core Coq datatypes. Tactics, AST, kernel terms and
types are all serialized. SerAPI also provide an API to manipulate and
query "Coq documents".
## How many ASTs does Coq have?
That's a very interesting question! The right answer is: _countably many_!
Logician jokes aside, the truth is that Coq features an _extensible_
AST. While this gives great power to plugins, it means that consumers
of the AST need to design their tools to support an _open_ AST.
Coq's core parsing AST is called `vernac_expr`. This type represents
the so-called "Coq vernaculars". Plugins can extend the "vernacular",
so you should be prepared to handle arbitrary content under the
`VernacExtend` constructor. Such arbitrary content is called in Coq
terminology "generic arguments".
### Interpretation and Terms
After parsing, a term will undergo two elaboration phases before it
will reach "kernel" form. The top-level parsing type for terms is
`constr_expr`, which is then _internalized_ to a `glob_constr`. This
process will perform:
- Name resolution. Example `λ x : nat. x` is resolved to `λ (x: Init.nat), Var 1`
[using debruijn for bound variables].
- Notation interpretation. For example, `a + b` is desugared to `Nat.add a b`.
- Implicit argument resolution. For example `fst a` is desugared to
`@fst _ _ a` [note the holes].
- Some desugaring of pattern-matching problems also takes place.
The next step is type inference (called pretyping in Coq, as "typing"
is used for the kernel-level type checking), which will turn a term
in `glob_constr` form into a full-typed `Constr.t` value. `Constr.t`
are the core terms manipulated by Coq's kernel and tactics.
When a _generic argument_ is added to Coq's AST, we must also provide
the corresponding _internalization_ and _pretyping_ functions. To that
purpose, generic arguments have associated 3-levels, `raw`, `glb`, and
`top` which correspond to parsing-level, internalized-level, and
kernel-level.
Thus, a generic argument of type `foo`, may carry 3 different OCaml
types depending on the level the type is. This is used for example to
define the AST of _LTAC_ tactics, where the expression `pose s := foo`
with `foo` initially a `constr_expr` will undergo interpretation and
inference up to a term with a fully elaborated `foo` term.
vendor/coq-serapi/LICENSE 0 → 100644
View file @ 2a40a0b1
Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
Upstream-Name: coq-serapi
Upstream-Contact: Emilio J. Gallego Arias <e@x80.org>
Source: https://github.com/ejgallego/coq-serapi
License: LGPL-2.1+
Copyright: 2016-2022, MINES ParisTech / Inria
Authors: Emilio J. Gallego Arias
Files: notes/*
License: LGPL-2.1+ / CC-BY-SA 3.0
Files: jscoq/*
License: GPL-3+
Files: tests/genarg/*
Authors: Karl Palmskog
Licence: Derived from many projects as test cases, falls into fair-use
Comment: the intent is to be compatible with Coq's license. Note that
the LGPL-2.1+ allows to treat the code as GPL-3+ , and we favor
that. In some cases, like when linking with jsCoq's code or other code
that is GPL-3 only, the resulting .js or binaries files will be GPL-3.
vendor/coq-serapi/Makefile 0 → 100644
View file @ 2a40a0b1
.PHONY: clean all serlib sertop sercomp force js-dist js-release build build-install test doc
# Leave empty to use OPAM-installed Coq
SERAPI_COQ_HOME ?=
# SERAPI_COQ_HOME=/home/egallego/external/coq-v8.17/_build/install/default/lib/
ifneq ($SERAPI_COQ_HOME,)
export OCAMLPATH := $(SERAPI_COQ_HOME):$(OCAMLPATH)
SP_PKGS=coq-serapi
else
SP_PKGS=coq-serapi
endif
all: build
GITDEPS=$(ls .git/HEAD .git/index)
sertop/ser_version.ml: $(GITDEPS)
echo "let ser_git_version = \"$(shell git describe --tags || cat VERSION)\";;" > $@
build:
dune build --root . --only-packages=$(SP_PKGS) @install
check:
dune build --root . @check
build-install:
dune build coq-serapi.install
test:
dune runtest --root .
doc:
dune build @doc-private @doc
browser:
google-chrome _build/default/_doc/_html/index.html
sertop: build
dune exec -- rlwrap sertop
#####################################################
# Javascript support
#####################################################
# JS
JSDIR=jscoq/coq-libjs
JSFILES=$(addprefix $(JSDIR)/,mutex.js unix.js str.js coq_vm.js)
JSCOQ_DEBUG=no
JSOO_OPTS=
ifeq "${JSCOQ_DEBUG}" "yes"
JSOO_OPTS+= --pretty --noinline --disable shortvar --debug-info
endif
js:
mkdir -p js
force:
_build/default/sertop/sertop_js.bc: force
dune build --profile=release sertop/sertop_js.bc
js/sertop_js.js: js _build/default/sertop/sertop_js.bc
js_of_ocaml --dynlink +nat.js +dynlink.js +toplevel.js $(JSOO_OPTS) $(JSFILES) _build/default/sertop/sertop_js.bc -o js/sertop_js.js
# We cannot use the separate compilation mode due to Coq's VM: libcoqrun.a
js-dune:
dune build --profile=release sertop/sertop_js.bc.js
js-dist:
rsync -avp --exclude=.git --delete ~/research/jscoq/coq-pkgs/ js/coq-pkgs
js-release:
rsync -avp --exclude=*~ --exclude=.git --exclude=README.md --exclude=get-hashes.sh --delete js/ ~/research/jscoq-builds
#####################################################
# Misc
clean:
rm -f sertop/ser_version.ml
dune clean
demo-sync:
rsync -avzp --delete js/ /home/egallego/x80/rhino-hawk/
cp /home/egallego/x80/rhino-hawk/term.html /home/egallego/x80/rhino-hawk/index.html
vendor/coq-serapi/README.md 0 → 100644
View file @ 2a40a0b1
## SerAPI: Machine-Friendly, Data-Centric Serialization for Coq
[![Build Status][action-badge]][action-link]
[![Zulip][zulip-badge]][zulip-link]
[action-badge]: https://github.com/ejgallego/coq-serapi/actions/workflows/ci.yml/badge.svg?branch=v8.16
[action-link]: https://github.com/ejgallego/coq-serapi/actions/workflows/ci.yml?query=branch%3Av8.16
[zulip-badge]: https://img.shields.io/badge/Zulip-chat-informational.svg
[zulip-link]: https://coq.zulipchat.com/#narrow/stream/256331-SerAPI
To install with opam:
```
$ opam install coq-serapi
$ sertop --help
```
Alternatively, if you use Nix:
```
$ nix-shell -p coq_8_13 coqPackages_8_13.serapi
$ sertop --help
```
SerAPI is a library for machine-to-machine interaction with the [Coq proof assistant](https://coq.inria.fr),
with particular emphasis on applications in IDEs, code analysis tools, and machine learning.
SerAPI provides automatic serialization of Coq's internal
[OCaml](https://ocaml.org) datatypes from/to [JSON](https://www.json.org) or
[S-expressions](https://en.wikipedia.org/wiki/S-expression) (sexps).
SerAPI is a proof-of-concept and should be considered
alpha-quality. However, it is fully functional and supports, among
other things, asynchronous proof checking, full-document parsing, and
serialization of Coq's core datatypes. SerAPI can also be run as
[WebWorker](https://developer.mozilla.org/en-US/docs/Web/API/Web_Workers_API/Using_web_workers)
thread, providing a self-contained Coq system inside the
browser. Typical load times in Google Chrome are less than a second.
The main design philosophy of SerAPI is to **make clients' lives easy**,
by providing a convenient, robust interface that hides most
of the scary details involved in interacting with Coq.
Feedback from Coq users and developers is very welcome and _intrinsic_
to the project. We are open to implementing new features and exploring
new use cases.
### Documentation and Help:
- [Protocol Documentation](http://ejgallego.github.io/coq-serapi/coq-serapi/Serapi/Serapi_protocol/)
- [interface file](serapi/serapi_protocol.mli)
- [SerAPI's FAQ](FAQ.md)
- [technical report](https://hal-mines-paristech.archives-ouvertes.fr/hal-01384408)
- [issue tracker](https://github.com/ejgallego/coq-serapi/issues)
- [Zulip chat](https://coq.zulipchat.com/#narrow/stream/256331-SerAPI)
- [Gitter chat](https://gitter.im/coq-serapi/Lobby) channel (legacy)
- [mailing list](https://x80.org/cgi-bin/mailman/listinfo/jscoq)
**API WARNING:** _The protocol is experimental and may change often_.
### Quick Overview and Install:
SerAPI can be installed as the [OPAM](https://opam.ocaml.org) package `coq-serapi`
or the [Nix](https://nixos.org) package `coqPackages_8_13.serapi`.
See [build instructions](notes/build.md) for manual installation. The experimental
[in-browser version](https://x80.org/rhino-hawk) is also online.
SerAPI provides an interactive "Read-Print-Eval-Loop" `sertop`, a
batch-oriented compiler `sercomp`, and a batch-oriented tokenizer `sertok`.
See the manual pages and `--help` pages of each command for more details.
To get familiar with SerAPI we recommend launching the `sertop` REPL,
as it provides a reasonably human-friendly experience:
```
$ rlwrap sertop --printer=human
```
You can then input commands. `Ctrl-C` will interrupt a busy Coq
process in the same way it interrupts `coqtop`.
The program `sercomp` provides a command-line interface to some
key functionality of SerAPI and can be used for batch processing
of Coq documents, e.g., to serialize Coq source files from/to lists of
S-expressions of Coq vernacular sentences. See `sercomp --help` for some
usage examples and an overview of the main options. The program `sertok`
provides similar functionality at the level of Coq source file tokens.
### Protocol Commands:
Interaction with `sertop` is done using _commands_, which can be optionally tagged in the form of `(tag cmd)`; otherwise, an automatic tag will be assigned.
For every command, SerAPI **will always** reply with `(Answer tag Ack)` to indicate that the command was successfully parsed and delivered to Coq, or with a `SexpError` if parsing failed.
There are three categories of [commands](serapi/serapi_protocol.mli#L147):
- **Document manipulation:** `Add`, `Cancel`, `Exec`, ...: these commands instruct Coq to perform some action on the current document.
Every command will produce zero or more different _tagged_ [answers](serapi/serapi_protocol.mli#52), and a final answer `(Answer tag Completed)`, indicating that there won't be more output.
SerAPI document commands are an evolution of the OCaml STM API, [here](https://github.com/ejgallego/jscoq/blob/master/etc/notes/coq-notes.md) and [here](https://github.com/siegebell/vscoq/blob/master/CoqProtocol.md) you can find a few informal notes on how it works. We are working on a more detailed specification, for now you can get some more details in the issue tracker.
- **Queries:** `(Query ((opt value) ...) kind)`:
Queries stream Coq objects of type `kind`. This can range from options, goals and hypotheses, tactics, etc.
The first argument is a list of options: `preds` is a list of conjunctive filters, `limit` specifies how many values the query may return.
`pp` controls the output format: `PpSer` for full serialization, or `PpStr` for "pretty printing". For instance:
```lisp
(tag (Query ((preds (Prefix "Debug")) (limit 10) (pp PpSexp)) Option))
```
will stream all Coq options that start with "Debug", limiting to the first 10 and printing the full internal Coq datatype:
```lisp
(CoqOption (Default Goal Selector)
((opt_sync true) (opt_depr false) (opt_name "default goal selector")
(opt_value (StringValue 1))))
...
```
Options can be omitted, as in: `(tag (Query ((limit 10)) Option))`, and
currently supported queries can be seen [here](serapi/serapi_protocol.mli#L118)
- **Printing:** `(Print opts obj)`: The `Print` command provides access to the Coq pretty printers.
Its intended use is for printing (maybe IDE manipulated) objects returned by `Query`.
### Roadmap and Developer organization:
SerAPI is organized in branches corresponding to upstream Coq
versions; usually, branch v8.XX is compatible with Coq 8.XX, and
corresponds to SerAPI 0.XX. These branches are stable and can be
relied upon.
The branch `main` tracks Coq `master` branch, and it is not a stable
branch; force pushes and random rebases can happen there; handle with
care!
We are working on fixing this problematic setup, which is that way as
in the past such branch used to be "private", but now that SerAPI is
in Coq's CI the development workflow has changed, with developer
submitting PRs to it.
These days, most work related to SerAPI is directly happening over
[Coq's upstream](https://github.com/coq/coq) itself. The main
objective is to improve the proof-document model; building a rich
query language will be next. See the [roadmap issue]() in our bug
tracker for more information about roadmap and the [Developer
Information](#Developer-information) section for more details on the
development setup.
### Clients and Users:
SerAPI has been used in a few contexts already, we provide a few
pointers here, feel free to add your own!
- [jsCoq](https://github.com/ejgallego/jscoq) allows you to run Coq in
your browser. jsCoq is the predecessor of SerAPI and will shortly be
fully based on it.
- [mCoq](https://github.com/EngineeringSoftware/mcoq) is a tool for mutation analysis
of Coq projects, based on serializing and deserializing Coq code via SerAPI.
See the accompanying [tool paper](https://users.ece.utexas.edu/~gligoric/papers/JainETAL20mCoqTool.pdf),
and the [research paper](https://users.ece.utexas.edu/~gligoric/papers/CelikETAL19mCoq.pdf)
which describes and evaluates the technique.
- [elcoq](https://github.com/cpitclaudel/elcoq), an emacs technology
demo based on SerAPI by [Clément Pit-Claudel](https://github.com/cpitclaudel). `elcoq` is not fully
functional but illustrates some noteworthy features of SerAPI.
- [PeaCoq](https://github.com/Ptival/PeaCoq), a Coq IDE for the
browser, has an experimental branch that uses SerAPI.
- [GrammaTech's Software Evolution Library (SEL)](https://grammatech.github.io/sel/)
provides tools for programmatically modifying and evaluating software. SEL operates
over multiple software representations including source code in
several languages and compiled machine code. Its Coq module uses
SerAPI to serialize Coq source code into ASTs, which are parsed into
Common Lisp objects for further manipulation. GrammaTech uses this
library to synthesize modifications to software so that it satisfies
an objective function, e.g., a suite of unit tests.
SerAPI support was added to SEL by Rebecca Swords.
- [CoqGym](https://github.com/princeton-vl/CoqGym) is a Coq-based learning environment for theorem proving.
It uses SerAPI to interact with Coq and perform feature-extraction. Its author notes:
> CoqGym relies heavily on SerAPI for serializing the internal structures of Coq.
> I tried to use Coq's native printing functions when I started with this project,
> but soon I found SerAPI could save a lot of the headaches with parsing Coq's output.
> Thanks to SerAPI authors, this project wouldn't be possible (or at least in its current form) without SerAPI.
See also the [paper](https://arxiv.org/abs/1905.09381) describing CoqGym.
- [Proverbot9001](https://github.com/UCSD-PL/proverbot9001) is a proof search system based on machine
learning techniques, and uses SerAPI to interface with Coq.
See also the [paper](https://arxiv.org/abs/1907.07794) describing the system.
- [Roosterize](https://github.com/EngineeringSoftware/roosterize) is a tool for
suggesting lemma names in Coq projects based on machine learning.
See the [paper](https://arxiv.org/abs/2004.07761) describing the technique and tool.
Additional paper with demo: https://arxiv.org/abs/2103.01346 .
- The [paper](https://arxiv.org/abs/2006.16743) _Learning to Format Coq Code Using Language Models_
implements a Coq code formatter.
- [MathComp corpus](https://github.com/EngineeringSoftware/math-comp-corpus) is a machine learning
dataset based on the [Mathematical Components](https://math-comp.github.io/) family of Coq projects,
and includes several machine-readable representations of Coq code generated via SerAPI.
The dataset was used to train and evaluate the Roosterize tool.
- A Python interface for SerAPI can be found at [PyCoq](https://github.com/IBM/pycoq)
- A direct Python interface to Coq, using `serlib` can be found at https://github.com/ejgallego/pyCoq
- SerAPI is being used to improve the Coq regression proof
selection tool [iCoq](https://cozy.ece.utexas.edu/icoq/),
see the [paper](https://users.ece.utexas.edu/~gligoric/papers/CelikETAL17iCoq.pdf).
- SerAPI is being used in additional software testing and machine learning projects; we will
update this list as papers get out of embargo.
### Quick Demo (not always up to date):
```lisp
$ rlwrap sertop --printer=human
(Add () "Lemma addn0 n : n + 0 = n. Proof. now induction n. Qed.")
> (Answer 0 Ack)
> (Answer 0 (Added 2 ((fname "") (line_nb 1) (bol_pos 0) (line_nb_last 1) (bol_pos_last 0) (bp 0) (ep 26))
> NewTip))
> ...
> (Answer 0 (Added 5 ... NewTip))
> (Answer 0 Completed)
(Exec 5)
> (Answer 1 Ack)
> (Feedback ((id 5) (route 0) (contents (ProcessingIn master))))
> ...
> (Feedback ((id 5) (route 0) (contents Processed)))
> (Answer 1 Completed)
(Query ((sid 3)) Goals)
> (Answer 2 Ack)
> (Answer 2
> (ObjList ((CoqGoal ((fg_goals (((name 5) (ty (App (Ind ...))))
(bg_goals ()) (shelved_goals ()) (given_up_goals ()))))))
> (Answer 2 Completed)
(Query ((sid 3) (pp ((pp_format PpStr)))) Goals)
> (Answer 3 Ack)
> (Answer 3 (ObjList ((CoqString
> "\
> \n n : nat\
> \n============================\
> \nn + 0 = n"))))
> (Answer 3 Completed)
(Query ((sid 4)) Ast)
> (Answer 4 Ack)
> (Answer 4 (ObjList ((CoqAst ((((fname "") (line_nb 1) (bol_pos 0) (line_nb_last 1)
> (bol_pos_last 0) (bp 34) (ep 50)))
> ...
> ((Tacexp
> (TacAtom
> (TacInductionDestruct true false
> ...
> (Answer 4 Completed)
(pp_ex (Print ((sid 4) (pp ((pp_format PpStr)))) (CoqConstr (App (Rel 0) ((Rel 0))))))
> (Answer pp_ex Ack)
> (Answer pp_ex(ObjList((CoqString"(_UNBOUND_REL_0 _UNBOUND_REL_0)"))))
(Query () (Vernac "Print nat. "))
> (Answer 6 Ack)
> (Feedback ((id 5) (route 0) (contents
> (Message Notice ()
> ((Pp_box (Pp_hovbox 0) ...)
> (Answer 6 (ObjList ()))
> (Answer 6 Completed)
(Query () (Definition nat))
> (Answer 7 Ack)
> (Answer 7 (ObjList ((CoqMInd (Mutind ....)))))
> (Answer 7 Completed)
```
### Technical Report:
There is a brief [technical report](https://hal-mines-paristech.archives-ouvertes.fr/hal-01384408)
describing the motivation, design, and implementation of SerAPI. If you are using
SerAPI in a project, please cite the technical report in any related publications:
```bibtex
@techreport{GallegoArias2016SerAPI,
title = {{SerAPI: Machine-Friendly, Data-Centric Serialization for Coq}},
author = {Gallego Arias, Emilio Jes{\'u}s},
url = {https://hal-mines-paristech.archives-ouvertes.fr/hal-01384408},
institution = {MINES ParisTech},
year = {2016},
month = Oct,
}
```
## Developer Information
### Technical Details
SerAPI has four main components:
- `serapi`, an extended version of the current IDE protocol;
- `serlib`, a library providing automatic de/serialization of most Coq data structures using `ppx_conv_sexp`. This should be eventually incorporated into Coq itself. Support for `ppx_deriving_yojson` is work in progress;
- `sertop`, `sertop_js`, toplevels offering implementations of the protocol;
- `sercomp`, `sertok`, command-line tools providing access to key features of `serlib`.
Building your own toplevels using `serlib` and `serapi` is encouraged.
### Advanced Use Cases
With a bit more development effort, you can also:
- Use SerAPI as an OCaml library. The low-level serialization library
[`serlib/`](/serlib) and the higher-level SerAPI protocol in
[`serapi/serapi_protocol.mli`](/serapi/serapi_protocol.mli) can be
linked standalone.
- Use SerAPI's web worker [JavaScript Worker](https://developer.mozilla.org/en-US/docs/Web/API/Web_Workers_API/Using_web_workers)
from your web/node application. In this model, you communicate with SerAPI using
the typical `onmessage/postMessage` worker API. Ready-to-use builds
may be found at
[here](https://github.com/ejgallego/jscoq-builds/tree/serapi), we
provide an example REPL at: https://x80.org/rhino-hawk
We would also like to provide a [Jupyter/IPython kernel](https://github.com/ejgallego/coq-serapi/issues/17).
### Developer/Users Mailing List
SerAPI development is mainly discussed [on GitHub](https://github.com/ejgallego/coq-serapi)
and in the [Gitter channel](https://gitter.im/coq-serapi/Lobby).
You can also use the jsCoq mailing list by subscribing at:
https://x80.org/cgi-bin/mailman/listinfo/jscoq
The mailing list archives should also be available at the Gmane group:
`gmane.science.mathematics.logic.coq.jscoq`. You can post to the list
using nntp.
## Acknowledgments
SerAPI has been developed at the
[Centre de Recherche en Informatique](https://www.cri.ensmp.fr) of
[MINES ParisTech](http://www.mines-paristech.fr/) (former École de
Mines de Paris) and was partially supported by the
[FEEVER](http://www.feever.fr) project.
vendor/coq-serapi/ROADMAP.md 0 → 100644
View file @ 2a40a0b1
### Full document parsing.
- Full asynchronous `Add/Cancel` protocol.
=> Add a cache so users can efficiently send full documents.
### Better Locate
- Implement Locate -> "file name where the object is defined".
- Improve locate [EJGA: how?]
- Help with complex codepaths:
Load Path parsing and completion code is probably one of the most complex part of company-coq
### Completion / Naming
- Improve the handling of names and environments, see
`Coq.Init.Notations.instantiate` vs `instantiate`, the issue of
`Nametab.shortest_qualid_of_global` is a very sensible one for IDEs
Maybe we could add some options `Short`, `Full`, `Best` ? ...
Or we could even serialize the naming structure and let the ide decide if we export the current open namespace.
### Benchmarking
- add bench option to queries commands
basically (bench (any list of serapi commands))
will return BenchData
- Define timing info? Maybe this is best handled at the STM level.
### Misc
- Redo Query API, make Query language a GADT.
- Support regexps in queries.
- Would be easy to get a list of vernacs? Things like `Print`, `Typeclasses eauto`, etc.
=> ppx to enumerate datatypes. Write the help command with this and also Clément suggestions about Vernac enumeration.
- enable an open CoqObject tag for plugin use (see coq/coq#209 ) ?
- Checkstyle support.
vendor/coq-serapi/VERSION 0 → 100644
View file @ 2a40a0b1
%%VERSION%%
vendor/coq-serapi/build-js.sh 0 → 100755
View file @ 2a40a0b1
#!/bin/bash
OCAML_VER=4.06.1
# build 32 bits parts
opam switch $OCAML_VER+32bit
eval `opam config env`
# Change to your jscoq location
export SERAPI_COQ_HOME=/home/egallego/research/jscoq/coq-external/coq-v8.8+32bit/
make js/sertop_js.js
make js-dist
vendor/coq-serapi/coq-serapi.opam 0 → 100644
View file @ 2a40a0b1
opam-version: "2.0"
maintainer: "e@x80.org"
homepage: "https://github.com/ejgallego/coq-serapi"
bug-reports: "https://github.com/ejgallego/coq-serapi/issues"
dev-repo: "git+https://github.com/ejgallego/coq-serapi.git"
license: "GPL-3.0-or-later"
doc: "https://ejgallego.github.io/coq-serapi/"
synopsis: "Serialization library and protocol for machine interaction with the Coq proof assistant"
description: """
SerAPI is a library for machine-to-machine interaction with the
Coq proof assistant, with particular emphasis on applications in IDEs,
code analysis tools, and machine learning. SerAPI provides automatic
serialization of Coq's internal OCaml datatypes from/to JSON or
S-expressions (sexps).
"""
authors: [
"Emilio Jesús Gallego Arias"
"Karl Palmskog"
"Clément Pit-Claudel"
"Kaiyu Yang"
]
depends: [
"ocaml" { >= "4.09.0" }
"coq" { !pinned & >= "8.17" & < "8.18" }
"cmdliner" { >= "1.1.0" }
"ocamlfind" { >= "1.8.0" }
"sexplib" { >= "v0.13.0" }
"dune" { >= "2.0.1" }
"ppx_import" { build & >= "1.5-3" & < "2.0" }
"ppx_deriving" { >= "4.2.1" }
"ppx_sexp_conv" { >= "v0.13.0" }
"ppx_compare" { >= "v0.13.0" }
"ppx_hash" { >= "v0.13.0" }
"yojson" { >= "1.7.0" }
"ppx_deriving_yojson" { >= "3.4" }
]
conflicts: [
"result" {< "1.5"}
]
build: [ "dune" "build" "-p" name "-j" jobs ]
vendor/coq-serapi/dune 0 → 100644
View file @ 2a40a0b1
(env
(dev (flags :standard))
(release (flags :standard)))
(install
(section share_root)
(files (sertop.el as emacs/site-lisp/sertop.el)))
vendor/coq-serapi/dune-project 0 → 100644
View file @ 2a40a0b1
(lang dune 2.0)
(formatting (enabled_for ocaml))
(name coq-serapi)
vendor/coq-serapi/extcoq/dune 0 → 100644
View file @ 2a40a0b1
(library
(name extcoq)
(public_name coq-serapi.extcoq)
(wrapped false)
(libraries coq-core.vernac coq-core.stm))