Indexing and search for LambdaPi

[sacerdot]

This PR adds:

• indexing and search commands in the CLI, as queries and provided by a webserver
• a query language to compose basic queries
• new options --no-sr-check, --rules, --port
• the record type Eval.config is extended with a new field allowing to specify which dtree to use for each symbol

The last two modifications allow to later implement something similar to dkmeta in lambdapi.

TODO:

• [x] CI fails with ocaml < 4.14.1
• [x] update CHANGES.md
• [x] update AUTHORS.md
• [x] @fblanqui test locate/search/search-query commands (VSCode is broken again for me)
• [x] update emacs and vscode
• [x] doc --no-sr-check
• [ ] @fblanqui reorganize options.rst with a section for each command ?
• [x] @sacerdot add examples in doc/query_language.rst
• [x] update comments of modified functions
• [x] make sanity_check
• [x] update BNF
• [x] update doc of command line arguments
• [x] update doc of lambdapi queries
• [x] add comment in doc that results of search may be not well typed
• [x] fix hard-coded string "LPSearch" in parse_term_string in lambdapi.ml: I have nothing better to put there, it stays like that
• [x] fix hard-coded Indexing.dbpath and meta-rules file
• [x] add option --meta-rules for reading file LPSearch.lp
• [x] rename command resolve by locate
• [x] put keywords in alphabetic order
• [x] replace assert false by fatal whenever possible
• [x] in lambdapi.ml, locate_cmd should take an identifier and not a string
• [x] replace LPSearch.dk by LPSearch.lp
• [x] when reading LPSearch.lp, fail if an identifier is not qualified
• [x] allow the search query in the middle of a proof, using the variables of the proof context; turn metavariables into patterns?
• [x] be sure to quote all dedukti/lambdapi snippets that are pasted to the web page
• [x] add cli/query command for the query language
• [x] remove "search" in favour of the query language? (maybe yes) same for locate? (probably not)
• [x] allow to start the webserver on a different port
• [x] rename the webserver to websearch
• [x] branch the query language doc to the main doc
• [x] test indexing and search on lambdapi files (in particular test path restriction of the query language)

index file:

• define a default place for the index files, for instance ~/.lambdapi/LPSearch.db and ~/.lambdapi/LPSearch.lp
• better: use dune site for use opam compatible places

future work (not for this PR):

• [ ] remove fix in pos.ml for handling https://github.com/Deducteam/lambdapi/issues/1001
• [ ] add rules to undo HOL encoding
• [x] add a query language
• [ ] more WHEN/HOW specifications? (e.g. in conclusion or spine)
• [x] more precise matching information (in particular: in conclusion/hypothesis)
• [ ] even more precise information: in conclusion of hypothesis
• [x] for more precise results, allow a variant of index-matching where an IHOLE can be matched only by an IVar; this "undoes" the "modus ponens" step used during indexing
• [ ] order search results according to precision of the matching (larger patterns) or other criteria