Skip to content

Commit 49e1877

Browse files
feat: search priorities (#837)
Adds prioritization to search results, slightly boosting searches for names and tactic names while down-prioritizing release notes. Relies on leanprover/verso#844.
1 parent ab5be92 commit 49e1877

3 files changed

Lines changed: 12 additions & 1 deletion

File tree

Main.lean

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -48,4 +48,14 @@ where
4848
logo := some "/static/lean_logo.svg",
4949
sourceLink := some "https://github.com/leanprover/reference-manual",
5050
issueLink := some "https://github.com/leanprover/reference-manual/issues",
51+
searchPriorities := {
52+
domains := .ofList [
53+
(`Verso.Genre.Manual.doc.tech, 65),
54+
(`Verso.Genre.Manual.doc, 60),
55+
(`Verso.Genre.Manual.doc.tactic, 60),
56+
(`Verso.Genre.Manual.doc.tactic.conv, 60),
57+
(`Verso.Genre.Manual.doc.option, 60),
58+
(`Verso.Genre.Manual.example, 60),
59+
]
60+
},
5161
}

Manual/Releases.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,7 @@ open Verso.Genre
5454
tag := "release-notes"
5555
file := "releases"
5656
number := false
57+
searchPriority := 10
5758
%%%
5859

5960
This section provides release notes about recent versions of Lean. When updating to a new version, please

lake-manifest.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "",
8-
"rev": "5cd850bfa36353d83e0abd638696b51c68c5adff",
8+
"rev": "06759f86fe54122ba3c081f40ed1cd24cffb8832",
99
"name": "verso",
1010
"manifestFile": "lake-manifest.json",
1111
"inputRev": "main",

0 commit comments

Comments
 (0)