Thanks for all the feedback. We've been working a way on tweaking the
search results. We're working on optimising the search results right now,
and we've uploaded the latest batch of improvements. Searching the comment
text is pretty good and the theorem names are easy to match (you can try
searching theorem names to see if it gets it right). Trying to match the mm
code is harder, it's difficult to work out how to get it to understand
enough about the sort of thing you are inputting to get useful results.
Have a go with the new version if you are interested, try putting mm
searches in quotes, that seems to help things match pretty well. If you
want to tweak the search yourself you can, you can right click on the page,
save the source and then edit this section
bool: {
should: {
multi_match: {
// type: "best_fields",
query: query,
// default_operator: "AND",
fields: [
"name^4",
// "usage",
"source^2",
"proof^2",
// "statementNumber",
"comment^2",
"contributor",
// "date",
"statement^10",
"hypotheses^2",
// "optionalHypotheses",
// "requiredVariables",
// "allowedVariables",
// "containedVariables",
// "disjointPairs",
"html.comment^2",
"html.comment.metamath^2",
// "html.syntaxHints",
// "html.axioms",
// "html.dependencies",
// "html.usage",
"html.hypotheses^2",
"html.statement^2",
"html.proof^2",
],
boost: 100,
}
},
to change the weight given to different parts of the search.
To get a really good search we may need to index everything differently
however that might be too far for us at the moment. I think it's working
decently now so would be interested if people use it at all when actually
trying to prove something.
Norm re fonts and total results return those things seem pretty doable, we
just haven't got round to them yet :)
We've hosted the search on a free trial for another week or so, if anyone
thinks it's going to be useful to you then we can talk about how to get it
hosted more permanently.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/18f6f640-7840-44cb-b36f-efb2d78e370e%40googlegroups.com.
