Modularize PDBF elements

[IchbinkeinReh]

Modularize PDBF elements and implement a simple api that users can use to create their own PDBF elements

[wetneb]

Hi @IchbinkeinReh! Congratulations for this amazing project! I'd love to use it for my stuff, and if I understand this issue correctly it is exactly what I am looking for: I would like to define my own LaTeX/HTML elements. More specifically, I am thinking about integrating a proof assistant (https://github.com/ejgallego/jscoq) to evaluate proofs alongside a LaTeX document. If you have any hint about where to start, or how to help you expose a cleaner API, it would be fantastic.

Keep up the good work!

[IchbinkeinReh]

Hey, i'm no more directly responsible for the project, but i want to help you anyway. I really like the idea of integrating a proof assistant into the PDBF framework. Are you fluent int Java and/or Javascript? I would do the LaTeX implementation and if possible i can guide you through the things that you have to change in the Java and Js code

[wetneb]

Fantastic! I am familiar with Java and Javascript, yes. Help on the LaTeX would be more than welcome indeed :-)

I'm not quite sure what would be the most interesting widget to implement. One obvious thing to try would be to implement a textarea like the ones here: https://x80.org/rhino-coq/

But it is not clear to me that this would be very usable in a research paper (where only a few interesting parts of the formal development are shown in the paper). Anyway this is essentially an UI issue so once the basic machinery is in place it shouldn't be too hard to make it more usable.

[IchbinkeinReh]

Unfortunately i don't have time to help you right now. I will post another message in approximately 2 weeks when I have more free time.

If you want to start already you can fork the project and alter the implementation of the \sql command. Then you don't need to implement another command and can directly work on the JavaScript implementation. The file you need to change is "data/main.js". Remove Line 305-309 and write your Code. The sql String is in "json.type.I.queryB".

To test your implementation you need a debug pdbf document which you can get with the "--no-include-res" Option. Place the document you get in the data folder and open it. Then you can directly see if your Code works. You will currently need to manually add additional js files into the debug pdbf Element. You can simply add them with a Text Editor.

If you have questions let me know

[wetneb]

Thanks a lot! Yes it's not urgent of course! I will play a bit with it in the coming weeks.

[IchbinkeinReh]

@wetneb As promised, i worked a bit on integrating joq into pdbf. You can look at it in my fork at https://github.com/IchbinkeinReh/PDBF

Example code for jscoq usage is in minimal.tex You can download the build at https://github.com/IchbinkeinReh/PDBF/archive/gh-pages.zip

Current Limitations:

• coq-pkgs are not integrated into the pdbf document. therefore a internet connection is required
• jsCoq uses JavaScript ES6, therefore only up to date browsers are supported

If you want to give me feedback please open a new issue at https://github.com/IchbinkeinReh/PDBF/issues

Regards Patrick

[wetneb]

@IchbinkeinReh wow, that sounds great, thank you so much! I will have a look at it asap.