12.4 Coq_SearchIsos: information retrieval in a Coq proofs library
In the Coq distribution, there is also a separated and independant tool, called Coq_SearchIsos, which allows the search in accordance with SearchIsos(see section 5.2.7) in a Coq proofs library. More precisely, this program begins, once launched by coqtop -searchisos, loading lightely (by using specifications functions) all the Coq objects files (.vo) accessibles by the LoadPath (see section 5.5). Next, a prompt appears and four commands are then available:- SearchIsos
-
Scans the fixed context. - Time
-
Turns on the Time Search Display mode (see section 5.8.5). - Untime
-
Turns off the Time Search Display mode (see section 5.8.5). - Quit
-
Ends the coqtop -searchisos session.
When running coqtop -searchisos you can use the two options:
- -opt
-
Runs the native-code version of Coq_SearchIsos.
- -image file
-
This option sets the binary image to be used to be file instead of the standard one. Not of general use.