- Oct 01, 2023
-
-
Shachar Itzhaky authored
-
- Jul 15, 2023
-
-
Shachar Itzhaky authored
-
- Jun 21, 2023
-
-
Elad Kinsbruner authored
Signed-off-by:
Elad Kinsbruner <kinsbruner@campus.technion.ac.il>
-
- Apr 12, 2023
-
-
Shachar Itzhaky authored
-
- Jan 24, 2023
-
-
Emilio Jesus Gallego Arias authored
This is a large build-time improvement, moreover we can get rid of a lot of troublesome code regarding how to manage assets. `esbuild` has proven a great tool so far. Tested with both backends. We still keep the CLI and the WASM backend on webpack, the idea is to move them to esbuild in subsequent commits. CLI should use a native Coq instead, it is super-slow. We also disabled the `collab` and `ide-project` builds for now, re-adding before merging hopefully. The compatibility story with user .html pages needs to be revised, IMHO as this is a foundation for the LSP backend this is the time to drop support for some patterns we had in the past.
-
- Sep 21, 2022
-
-
Emilio Jesus Gallego Arias authored
We reorganize jsCoq's source code as to be more modular, in particular we start to place backend files under the `backend` directoy, and frontend files under `frontend`. Code as it now does work, note however that still quite a bit of work is needed. In particular, the headless frontend should get its own directory, the coq-jslib directory should go away, use more types, etc...
-
- Sep 09, 2022
-
-
Shachar Itzhaky authored
Changed codename, seems more temporally fitting.
-
- Aug 15, 2022
-
-
Emilio Jesus Gallego Arias authored
-
- Jun 19, 2022
-
-
Emilio Jesus Gallego Arias authored
This is broken due to `load_plugin` not being implemented yet. We need to think about how to fix that, likely just updating our library manager to include `META` files for the plugins should work, but we need to find out. The main relevant change for us in Coq 8.16 is that Coq now loads plugins using the `Fl_dynload` API. So now Coq, will make a request for `coq-core.plugins.ltac` instead of `ltac_plugin.cma`. `Fl_dynload` is a wrapper over `Dynlink.loadfile`, but will check `META` files for dependencies, and if plugins `A` depends on `B`, will load `B` first. This may be a problem for us, we need to figure how to handle that. One approach couuld be to replace the `Dynlink.dynload` stub with the proper javascript implementation so the `Fl_dynload` uses it implicitly. Another (temporal) alternative to get this working is just to ignore deps and implement `Ml_top.load_plugin` with a mapping. I have done that as Coq 8.16 still includes a "legacy" mode, which should work for some plugins, but not for all of them (coq-elpi for example requires this). The 3rd approach would be for us to reimplement `Fl_dynload` by locating the META files and parsing them, or storing this metadata in some other fashion.
-
- May 21, 2022
-
-
Shachar Itzhaky authored
-
- May 01, 2022
-
-
Shachar Itzhaky authored
-
- Apr 30, 2022
-
-
Shachar Itzhaky authored
-
- Apr 29, 2022
-
-
Shachar Itzhaky authored
-
- Jan 05, 2022
-
-
Shachar Itzhaky authored
-
- Sep 24, 2021
-
-
Emilio Jesus Gallego Arias authored
- Migrated patches for 8.14. - Up wacoq to 8.14 in docker image - install: 8.14 requires `coq-core` and `coq-stdlib` to be installed. - Set version 0.14.0.
-
- Sep 17, 2021
-
-
Shachar Itzhaky authored
Listed `coqoban` in affiliated packages.
-
- Aug 11, 2021
-
-
Shachar Itzhaky authored
-
- Aug 03, 2021
-
-
Shachar Itzhaky authored
-
- Jul 11, 2021
-
-
Shachar Itzhaky authored
Closes #241.
-
- Jul 07, 2021
-
-
Shachar Itzhaky authored
-
- Jul 06, 2021
-
-
Shachar Itzhaky authored
-
- Jun 09, 2021
-
-
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
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 18, 2021
-
-
Shachar Itzhaky authored
Thanks @mdnahas :D
-
- May 16, 2021
-
-
Shachar Itzhaky authored
(+ tiny style fix)
-
- May 08, 2021
-
-
Shachar Itzhaky authored
-
- Mar 04, 2021
-
-
Shachar Itzhaky authored
-
- Feb 14, 2021
-
-
Emilio Jesus Gallego Arias authored
We also bump some other libraries as to reduce non-deterministic developer switches.
-
- Feb 13, 2021
-
-
Emilio Jesus Gallego Arias authored
Nothing too remarkable, code-wise, but a big change upstream is the addition of `zarith` as a hard dependency. TODO: - update addons
-
- Jan 13, 2021
-
-
Shachar Itzhaky authored
When building on macOS + arm64, choose OCaml 4.10.2 automatically (4.08.x is not available).
-
- Nov 02, 2020
-
-
Shachar Itzhaky authored
-
- Sep 18, 2020
-
-
Shachar Itzhaky authored
For batch compilation, compile with `Stm.VoDoc` type. Terminate worker after batch finishes up.
-
- Aug 12, 2020
-
-
Shachar Itzhaky authored
-
- Aug 07, 2020
-
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
-
- Jul 18, 2020
-
-
Emilio Jesus Gallego Arias authored
This seems needed for Coq 8.12
-
Emilio Jesus Gallego Arias authored
-
- Apr 28, 2020
-
-
Emilio Jesus Gallego Arias authored
This includes some bug fixes and the upstreaming of Shachar's Str stub, so we can remove it.
-
Shachar Itzhaky authored
Previous behavior was to mark the whole sentence. Now, the location reported as part of `CoqExn` is used.
-
- Apr 08, 2020
-
-
Emilio Jesus Gallego Arias authored
Closes #141
-