Modular interfaces#4
Conversation
|
Thanks a lot for this PR, @yurug! I will do a proper review of the code as soon as possible, although I basically trust you on that side. Once the code is stabilized, could you add yourself as a contributor of the file you created/modified? Also, an interactive rebase would be neat to squash commits db97a55 in a27e1fc and 5a5a742 in a27e1fc |
lthms
left a comment
lthms
left a comment
There was a problem hiding this comment.
This is the first time I do a review for FreeSpec :).
Changes look good to me, thanks a lot! Before merging, there remains several small changes to do, I think:
- Use this occasion to comment a bit the Ocaml files (yours in priority, I can try to comment the
exec.mlfile latter) - Check whether there are missing license headers
- Add yourself when you contribute to a file, remove my name if you have created the file
I tried to comment your changes throughout my reading of them, hope this will be useful.
| * Copyright (C) 2018–2019 ANSSI | ||
| * | ||
| * Contributors: | ||
| * 2019 Thomas Letan <thomas.letan@ssi.gouv.fr> |
There was a problem hiding this comment.
I am not the contributor of this file, you are! :)
| let register_interfaces interface_initializer = | ||
| Queue.add interface_initializer initializers | ||
|
|
||
| let force_interface_registering () = |
There was a problem hiding this comment.
force_ sounds a bit “scary.” Can you justify this name when you will comment this PR?
There was a problem hiding this comment.
Explained in e8ce114. I hope this will clarify the situation.
| package "freespec-stdlib-console" ( | ||
|
|
||
| description = "Freespec Stdlib/Console Plugin" | ||
| version = "8.10" |
There was a problem hiding this comment.
Same here as before. Should it be 8.9?
lthms
added
the
kind | feature
Co-Authored-By: yurug <yrg@pps.univ-paris-diderot.fr>
Co-Authored-By: yurug <yrg@pps.univ-paris-diderot.fr>
|
Thanks. I think we are good to go. I will just try to run this PR on my laptop to see if everything goes well (I have little doubt), then we can squash everything into a single commit and merge that into master. |
In the first iteration of FreeSpec.Exec, the (singleton) set of interfaces was statically defined by the execution function within the ocaml code. Supporting an additional interface meant modifying this function accordingly. With this change, FreeSpec.Exec is now easily extensible by means of Coq plugins. GitHub PR: #4
2 participants
Here is a draft proposal for define new interfaces to FreeSpec by means of plugins.
The code is neither commented nor stabilized yet but it should give the idea.
@lthms any comment?