Skip to content
Snippets Groups Projects
  1. Apr 18, 2023
  2. Jan 24, 2023
  3. Oct 05, 2022
    • Shachar Itzhaky's avatar
      [refactor] Rearrange wasm deps. · 6f67e658
      Shachar Itzhaky authored
      All wasm binaries are read from `node_modules` directly, so there is no
      need for a `bin/` directory (this was a hack).
      
      The deps are collected in a meta-package `wacoq-deps`, which is
      published to NPM separately and should not change often.
      6f67e658
    • Shachar Itzhaky's avatar
      [refactor] Normalized worker paths. · 432f551b
      Shachar Itzhaky authored
      The wasm backend bytecode is now loaded
      from `backend/wasm` (and also linked
      accordingly).
      432f551b
  4. Oct 02, 2022
  5. Sep 21, 2022
    • Emilio Jesus Gallego Arias's avatar
      [jscoq] [build] Start of backend / frontend split. · 33544625
      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...
      33544625
  6. Aug 15, 2022
  7. May 06, 2022
  8. Aug 08, 2021
  9. Mar 04, 2021
    • Shachar Itzhaky's avatar
      [addon] Sharing content with Hastebin. · 397f0320
      Shachar Itzhaky authored
      This is phrased as an "addon"; I think that not only libraries can be
      "addons" but this kind of interop UI functionality should be as well.
      
      It does not mean that UI addons should be built outside of the jsCoq
      source tree like mathcomp & co.
      If they are small enough, they are ok where they are in `ui-js/addon`.
      397f0320
  10. Jan 30, 2021
  11. May 03, 2019
  12. Apr 24, 2019
    • Shachar Itzhaky's avatar
      [build] Set up a local switch. · 33c88ce6
      Shachar Itzhaky authored
      32-bit compilation is using switch jscoq+32bit. 64-bit compilation
      is using jscoq+64bit.
      Coq is cloned into _vendor+xxx directories by Coq version and word
      size, and so are add-ons.
      33c88ce6
  13. Apr 21, 2019
  14. Apr 20, 2019
  15. Apr 08, 2019
  16. Mar 30, 2019
    • Emilio Jesus Gallego Arias's avatar
      [build] Port build to Dune · 529bc4a0
      Emilio Jesus Gallego Arias authored
      We port the build system to Dune. This setup will integrate nicely
      with Coq 8.10, but until this arrives it also provides a few
      advantages:
      
      - better `.merlin` files, automatically generated,
      - clean build tree: all the artifacts go under _build,
      - modular organization of the development: we introduce a separate
        library for the JS Coq package manager.
      
      Note indeed that now all the build artifacts do live in
      `_build/default`; `make links` will allow you to serve pages in-tree.
      
      Pending:
      
      - fully split the libmngr build to its own repository.
      - libjs: implement recursive scan / get closer to Dune.
      529bc4a0
  17. Mar 13, 2019
    • Shachar Itzhaky's avatar
      BUGFIX: Log positioning and filtering. · 5a8517a8
      Shachar Itzhaky authored
      Enhanced the log icons, which were cropped.
      Added Coq and Github icons in toolbar.
      5a8517a8
    • Emilio Jesus Gallego Arias's avatar
      [jscoq] Switch to Web Workers. · ad3d8305
      Emilio Jesus Gallego Arias authored
      JsCoq now runs in a worker and communicates with coq-manager using
      messages and PPX serializers.
      
      We have reshaped the API quite a bit. We are very close towards
      convergence with SerAPI, from which we have imported quite a few ideas.
      
      The main changes are:
      
      - coq-manager now follows a fully reactive approach (as suggested by
        @cpitclaudel) The document model has also evolved.
      
        This implies a big improvement in ease of document handling. In
        particular, we do not wait for `Add`, we listen to feedback to color
        states, and we use the new `Cancel` API instead of `EditAt`.
      
      - The library manager is basically shared with serapi, and it has been
        greatly simplified.
      
      - The protocol features a more robust initialization procedure, even
        if a bit heavier on client side responsibilities.
      
      - We have removed jsmock, it is not useful anymore.
      
      Many, many hacks have been removed in favor of more principled
      solutions; still, we have quite a long way to go.
      
      This commit improves #13, helps a bit with #9 (now we can kill the web
      worker), and (in an non-optimal way yet) fixes #16.
      
      Pending items:
      
      + Pp.t rendering is just a prototype, we need to improve it and insert
        divs following the current box mode.
      
      + Pp.t normalization leaves a lot to be desired. We can likely
        normalize it Ocaml-side and produce a div. We could even use jsoo's
        Tyxml for that.
      
      - The invalidation, focus, and movement logic needs a bit more of
        work. In particular we need to streamline adding many sentences.
      
      Real interaction with the worker is pretty fine these days.
      
      - We allow to export the initial namespace as implicit.
      
        This will help closing #18.
      
        In general, it was an annoyance for the users, so we may follow
        upstream on this one for now. We will update collacoq to use the
        proper default, and keep the init page with the more lightweight
        setup.
      ad3d8305
  18. Nov 27, 2017
  19. Nov 26, 2017
  20. Jun 22, 2016
  21. May 03, 2016
  22. Feb 28, 2016
  23. Dec 08, 2015
  24. Dec 06, 2015
  25. Nov 10, 2015
  26. Aug 15, 2015
  27. Aug 14, 2015
  28. Jul 23, 2015
  29. Jul 06, 2015
  30. Jul 01, 2015
  31. May 12, 2015
Loading