- Aug 06, 2021
-
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
Broken by previous refactor.
-
Shachar Itzhaky authored
Including tweaks in a few other places.
-
- Aug 05, 2021
-
-
Shachar Itzhaky authored
Makes more sense and also cleaner.
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
Modified `doc_options` to accept lib names as "."-delimited strings.
-
Shachar Itzhaky authored
And so it begins.
-
Shachar Itzhaky authored
`SearchResults` now carrying `qualified_name`s instead of `full_path`s.
-
Shachar Itzhaky authored
-
- Aug 03, 2021
-
-
Shachar Itzhaky authored
Refactor `FormatPrettyPrint` (again)
-
Shachar Itzhaky authored
-
- Aug 01, 2021
-
-
Shachar Itzhaky authored
In cases where the element has a padding, as is the case with `div.coq-env`. The unit-test gallery has been updated to reflect this situation.
-
Shachar Itzhaky authored
Trying to be more faithful to what `Format` does: - take into account offset parameter defined on boxes. - adhere to left margin of containing box, when breaking lines. - be more declarative via CSS. I think this would handle #126.
-
- Jul 18, 2021
-
-
Shachar Itzhaky authored
Closes #203.
-
Shachar Itzhaky authored
Each snippet is now shown both before and after break adjustment.
-
- Jul 16, 2021
-
-
Shachar Itzhaky authored
Symbol format has changed, but respective methods have not been updated.
-
Shachar Itzhaky authored
In the landing page, due to the existence of bootstrap CSS.
-
- Jul 14, 2021
-
-
Shachar Itzhaky authored
Some of the instructions are duplicated from the README, but that's ok. The manual is not yet complete with all the features, but at least addresses #207. Closes #207.
-
- Jul 11, 2021
-
-
Shachar Itzhaky authored
Closes #241.
-
Shachar Itzhaky authored
Include full module path. Improve the presentation when multiple matches are found.
-
- Jul 08, 2021
-
-
Shachar Itzhaky authored
-
- Jul 07, 2021
-
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
-
- Jul 06, 2021
-
-
Shachar Itzhaky authored
I'm merging because the Dockerfile is now good enough for both CI and non-CI use. The SDK is still borked because 32-bit. Merde.
-
Shachar Itzhaky authored
-
- Jul 03, 2021
-
-
Shachar Itzhaky authored
These were created using the waCoq CLI from Coq 8.13.2 standard library. When more than one lemma matches a name, multiple results are shown. Not clear why there are duplicates (i.e. same long name).
-
- Jun 13, 2021
-
-
Emilio Jesús Gallego Arias authored
[build] Bump required compiler version to 4.12.0
-
- Jun 12, 2021
-
-
Shachar Itzhaky authored
For SF, when volumes are built separately and incrementally.
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
(For quick testing only)
-
- Jun 09, 2021
-
-
Emilio Jesus Gallego Arias authored
This still requires considerable work, but when ready it should solve parts of #69 and #121. As for now, we don't push the image to a registry yet; we ought to decide: - when to build the docker image [maybe only on main branches] - where to push it - what to include - a standard setup for addons CI, so they pull the image and then build and publish their own package - how this does integrate with npm, maybe we shouldn't push the image but just a npm package built using docker [so addons do get the correct binaries to push to npm too] Based on: https://github.com/marketplace/actions/build-and-push-docker-images
-
Emilio Jesus Gallego Arias authored
This should nicely support M1-based OSX ; unfortunately, it required loosening the constraint on `ppx_deriving_yojson` as to make it co-installable with `ppx_import`, but that's a minor issue. Note the new option system for OCaml Opam packages, thus selecting a 32bit compiler is done differently now.
-
Emilio Jesus Gallego Arias authored
-
Emilio Jesús Gallego Arias authored
[jscoq] Make protocol interpreter independent of worker code.
-
Emilio Jesus Gallego Arias authored
This is a small refactoring that places the protocol interpreter into its own file. This is done in preparation for the new printer. For now I didn't complicate things much, and I have kept the interpreter access to the `jsoo` libs, tho it would be easy to actually make it independent by handling the interrupt code in the worker side [by layering the protocols] Note that in this setup we are actually architecturally very close to just replacing our protocol by the SerAPI protocol, while I don't think we should do that, IMHO it is important to keep the component structure consistent about projects as SerAPI wants to reuse the library manager for example in its jsoo version. Another interesting TODO here would be to actually improve our worker handling by moving some of our tricks into jsoo upstream.
-
Emilio Jesús Gallego Arias authored
[build] [ci] Preliminary github actions support
-
Emilio Jesus Gallego Arias authored
This is just a basic building setup, for linux at the moment. Github Actions is way more powerful than travis, so we can improve many previous things of the setup, concretely: - re-add OSX build - generate a docker image - set a job for each addon, or create a push event so addons are built on their own repos Closes #224 Thanks to Jason Gross for the help with the SerAPI action.
-
- May 21, 2021
-
-
Shachar Itzhaky authored
It was carried over from sf by mistake.
-
Shachar Itzhaky authored
-