jscoq and book.py

[spitters]

jscoq was designed with literate programming in mind. Literature programming also motivated book.py / book.v We now have the beautiful jshott. However, the two ideas were never combined. @ejgallego would there be any obstacles to this?

[spitters]

For comparison. Here is an example of literate HoTT in agda. I guess for a better comparison with agda, we might also want Equations to work for HoTT.

[ejgallego]

I am not very knowledgeable about book.py etc.. but interacting with jscoq tends to be fairly easy, in general, calling a function the init function with all the code divs should work:

  <script src="ui-js/jscoq-loader.js" type="text/javascript"></script>
  <script type="text/javascript">
    var jscoq_ids  = ['...' ];
    var jscoq_opts = {
        editor: { mode: { 'company-coq': true }, keyMap: 'default' },
        init_pkgs: ['init'],
        all_pkgs:  ['init', 'hott']
    };
    /* Global reference */
    var coq;
    loadJsCoq(jscoq_opts.base_path)
        .then( () => coq = new CoqManager(jscoq_ids, jscoq_opts) );
  </script>

[Alizter]

So we sort of have this now with alyectron. Although, the user cannot go and edit proof scripts in the browser. I am however a bit sceptical that being able to edit HoTT proof scripts in a browser is a practical thing to do.

[ejgallego]

Hi @Alizter !

Indeed Alectyron does provide a very nice workflow for the literate document generation, jsCoq can offer similar functionality if you are able to setup your html, as it can provide goals on hover in a similar way, just live tho [which can be annoying for some long running stuff, tho it is easy to cache them in a json]

I am however a bit sceptical that being able to edit HoTT proof scripts in a browser is a practical thing to do.

I think so far we have found jsCoq to be extremely useful! Not for the most hardcore developers, but keep in mind that Coq is most used in education / summer schools, tutorials, etc... and for that is super practical; I guess if an interactive version of the HoTT book would be ever made with Coq as a backend, you would like to have interactivity. For SF works pretty well IMHO https://jscoq.github.io//ext/sf/ , and that keeping into account that we are basically not yet even at the alpha stage for that particular integration.

A direction I'm pursuing this year is having Coq documents integrate much better as first class citizens of the DOM object model, that will be mainly useful in visualization too, but the approach we have in mind is structural, and while it took a long time to bootstrap we are getting close to the phase we can get a prototype working.

[Alizter]

Hi @ejgallego, thank you for the detailed reply!

[which can be annoying for some long running stuff, tho it is easy to cache them in a json]

Yes, this is precisely why I said I was sceptical of its utility to us. I didn't mean to say it wasn't a useful teaching tool however!

For SF works pretty well IMHO https://jscoq.github.io//ext/sf/ , and that keeping into account that we are basically not yet even at the alpha stage for that particular integration.

The work being done with software foundations looks exciting!

A direction I'm pursuing this year is having Coq documents integrate much better as first class citizens of the DOM object model

I look forward to hearing more about these changes.

We should give some serious thought to using jscoq in our documentation at some point. I wonder what @JasonGross thinks about this.

[ejgallego]

We should give some serious thought to using jscoq in our documentation at some point. I wonder what @JasonGross thinks about this.

If you use standard tools [coqdoc] you will get it for free soon I hope.

Yes, this is precisely why I said I was sceptical of its utility to us. I didn't mean to say it wasn't a useful teaching tool however!

If the only problem is running time, having coqc output a json with the goals for each sentence is actually pretty easy to do, so jscoq could check if the json file exists and then load the goals.

Goals are stored in jscoq as a simple associative map sentence_id -> goal_info so there is not a lot of complexity there; as of today, the array starts empty, and in some particular points, jsCoq does issue a (Goal sid) call, asychronously.

When the goal information is received, it is just stored in the array, and if necessary, a refresh of the goal DOM element is re-scheduled, pretty standard stuff except for the state-less protocol [so for example Goal info answer does contains the parameters of the original query so no state on client side is required]