@pestun Here is a demo of how you can use options. I added in some boilerplate code that helps you easily make options for bools, ints and strings. Other things can also be done, but I strongly recommend that you restrict yourself to these datatypes.
Warning: In order to allow the system to properly register these options, you have to read them lazily (i.e. only when you really need them). Otherwise the desired option may not have been set yet. In this example this is ensured by checking options only in the empty function, which is called lazily.
In the benchmarking system, I have added options -inject string and -inject-file file, to which you can add arbitrary Coq vernacular. To test this demo, you can create a file Test.v:
Set Tactician Neural MyBool.
Set Tactician Neural MyInt 42.
Set Tactician Neural MyPassword "correct horse battery staple".
@pestun Here is a demo of how you can use options. I added in some boilerplate code that helps you easily make options for bools, ints and strings. Other things can also be done, but I strongly recommend that you restrict yourself to these datatypes.
Warning: In order to allow the system to properly register these options, you have to read them lazily (i.e. only when you really need them). Otherwise the desired option may not have been set yet. In this example this is ensured by checking options only in the
emptyfunction, which is called lazily.In the benchmarking system, I have added options
-inject stringand-inject-file file, to which you can add arbitrary Coq vernacular. To test this demo, you can create a fileTest.v:And then benchmark using
Alternatively, you can avoid creating the file and benchmark using