Add logs, transform ASCII to unicode in requests and listen to custom URLs #1244
Conversation
| @@ -178,6 +178,8 @@ websearch | |||
|
|
|||
| * ``--header <FILE.html>`` uses <FILE.html> as header of the search engine web page. | |||
|
|
|||
| * ``--url <STRING>`` tells the server to accept requests only on URLs using path ``<STRING>`` (for instance ``localhost:8080/<STRING>``). Use ``**`` to accept requests with any path. | |||
There was a problem hiding this comment.
I suggest to name the option to --restrict-url which is more informative.
I don't fully understand what this option does actually. Could you clarify the explanation?
In particular the occurrences 2 and 3 of <STRING> seems to represent two different variables.
What is the point of ** if you can get the same without using the option?
Why not interpreting <STRING> as regular expression?
In this case, you could call the option: --match-url tells the server to accept requests only on URLs matching <STRING> interpreted as a regular expression. Does the url always start with localhost:8080/?
There was a problem hiding this comment.
Thanks @fblanqui for your comments.
Please find the answers to your questions in the comments on src/tool/websearch.eml.ml
There was a problem hiding this comment.
I suggest to name the option to
--restrict-urlwhich is more informative.
Yes. what about --serve-urls-with-paths ? It is a bit long. We could shorten it and/or use short option letters such as -u or -s.
What is the point of
**if you can get the same without using the option?
/** is interpreted by the Dream framework as : accept requests from any PATH. / is interpreted as accept request from the root path only.
I could add : default is "" to accept requests only from the root path
| @@ -12,6 +12,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/). | |||
| - Added tactic eval which evaluates a term and interprets it as a tactic. This allows one to define tactics using rewriting. | |||
| - Added builtin String for string literals between double quotes. | |||
| - Added the `--header` flag to the `websearch` command | |||
| - Added the `url` flag to the `websearch` command | |||
| (*Common.Logger.set_debug true "e" ;*) | ||
| let interface = "0.0.0.0" in | ||
| Dream.run ~port ~interface | ||
| @@ Dream.logger | ||
| @@ Dream.memory_sessions | ||
| @@ Dream.router [ | ||
|
|
||
| Dream.get "/" |
There was a problem hiding this comment.
Currently, the webserver only accepts requests received on the root path of the server (the part after the first / in the url)
Does the url always start with
localhost:8080/?
No. This could be localhost when deployed locally or any other url when deployed remotely such as lambdapi.saclay.inria.fr (though in this particular case it is a it different because we use Apache to redirect request on localhost.
Port can be of course different from 8080 depending on what port is passed with option --port when starting the server.
In the current code of the server, you have Dream.get "\" and Dream.post "\" which means that the server only accepts requests on the root path (as designed by /). This means that, in the case of the server deployed on lambdapi.saclay.inria.fr, sending a GET or a POST request to lambdapi.saclay.inria.fr/, answers with the server web page but trying to connect to lambdapi.saclay.inria.fr/testing-intance you will get an error even though the host machine has been configured to accept request on that url.
Why not interpreting
<STRING>as regular expression?
Actually <STRING> is expressed in a sub language of the Dream framework. This is different from the regular expressions language. For instance ** matches [^ ]*, but Dream does not accept this regular expression to match Paths.
Most often, users will use three values :
**: to match all paths- empty string (default) : to match only root path
<aPath>: to match a particular path<aPath>
This been said. Three solutions exist :- Define the url option as a regular expression and transform it to the
Dreamsub language. This is complicated and not really useful. - match only the three cases described above. This is +/- simple but restricts the possibilities offered by
Dream. - Use the native
Dreamsub language : very simple and preserves all the possibilities of deployment offered byDreambut not all users ofLambdapiknow theDreamframework.
I could also hard code it to accept requests from all paths and get ride of the url option.
What do you think is the better option?
There was a problem hiding this comment.
As discussed offline, the option we will keep for now is to use the last option and document it more.
| @@ -178,6 +178,8 @@ websearch | |||
|
|
|||
| * ``--header <FILE.html>`` uses <FILE.html> as header of the search engine web page. | |||
|
|
|||
| * ``--url <STRING>`` tells the server to accept requests only on URLs using path ``<STRING>`` (for instance ``localhost:8080/<STRING>``). Use ``**`` to accept requests with any path. | |||
There was a problem hiding this comment.
I suggest to name the option to
--restrict-urlwhich is more informative.
Yes. what about --serve-urls-with-paths ? It is a bit long. We could shorten it and/or use short option letters such as -u or -s.
What is the point of
**if you can get the same without using the option?
/** is interpreted by the Dream framework as : accept requests from any PATH. / is interpreted as accept request from the root path only.
I could add : default is "" to accept requests only from the root path
This PR :
foralland->to unicode caractersΠand→in search queriesurlflag to thewebsearchcommand to accept request on URLs with custom paths (for instancelocalhost:8080/<STRING>)