From b9fbe2e78aecde8a3bd226c026da4e50de639811 Mon Sep 17 00:00:00 2001 From: Pranav Teegavarapu Date: Thu, 14 Nov 2024 04:20:36 -0800 Subject: [PATCH] moogle 2.0 + leandocsearch formatting formatting textbook links 2.0 --- vscode-lean4/loogleview/static/index.html | 54 +++--- vscode-lean4/moogleview/index.ts | 212 +++++++++++++++------- vscode-lean4/moogleview/static/index.css | 71 +++++++- vscode-lean4/moogleview/static/index.html | 18 +- 4 files changed, 258 insertions(+), 97 deletions(-) diff --git a/vscode-lean4/loogleview/static/index.html b/vscode-lean4/loogleview/static/index.html index 6fc431c1..c58cb7eb 100644 --- a/vscode-lean4/loogleview/static/index.html +++ b/vscode-lean4/loogleview/static/index.html @@ -27,52 +27,64 @@

Usage

  1. - By constant:
    - Real.sin finds all lemmas whose statement somehow mentions the sinefunction. + By constant:
    + Real.sin finds all lemmas whose statement somehow + mentions the sinefunction.

  2. - By lemma name substring:
    - "differ" finds all lemmas that have "differ" somewhere in their lemma name. + By lemma name substring:
    + "differ" finds all lemmas that have + "differ" somewhere in their lemma name.

  3. - By subexpression:
    - _ * (_ ^ _) finds all lemmas whose statements somewhere include a product where the second argument is raised to some power. + By subexpression:
    + _ * (_ ^ _) finds all lemmas whose statements + somewhere include a product where the second argument is raised to some power.

    - The pattern can also be non-linear, as in Real.sqrt ?a * Real.sqrt ?a + The pattern can also be non-linear, as in + Real.sqrt ?a * Real.sqrt ?a

    - If the pattern has parameters, they are matched in any order. Both of these will find List.map:
    - (?a -> ?b) -> List ?a -> List ?b
    + If the pattern has parameters, they are matched in any order. Both of these will find + List.map:
    + (?a -> ?b) -> List ?a -> List ?b
    List ?a -> (?a -> ?b) -> List ?b

  4. - By main conclusion:
    - |- tsum _ = _ * tsum _ finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape. + By main conclusion:
    + |- tsum _ = _ * tsum _ finds all lemmas where the + conclusion (the subexpression to the right of all → and ∀) has the given shape.

    - As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example, |- _ < _ → tsum _ < tsum _ will find tsum_lt_tsum even though the hypothesis f i < g i is not the last. + As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; + for example, |- _ < _ → tsum _ < tsum _ will + find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

- If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _ - would find all lemmas which mention the constants Real.sin - and tsum, have "two" as a substring of the - lemma name, include a product and a power somewhere in the type, - and have a hypothesis of the form _ < _ (if - there were any such lemmas). Metavariables (?a) are - assigned independently in each filter. + If you pass more than one such search filter, separated by commas Loogle will return lemmas which match + all of them. The search + Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _ would + find all lemmas which mention the constants Real.sin and tsum, have "two" as + a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis + of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned + independently in each filter.

Source code

-

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is currently -provided by Joachim Breitner <>.

+

+ You can find the source code for this service at + https://github.com/nomeata/loogle. The + https://loogle.lean-lang.org/ service is currently provided + by Joachim Breitner <>. +

View source code + ${hit.metadata.declaration_docstring ? `
${hit.metadata.declaration_docstring}
` : ''} +
${tempElement.innerHTML}
+ View source code
- ` + ` - this.results.appendChild(resultElement) + this.setupResultToggle(element) + } - const header = resultElement.querySelector('.result-header') - const content = resultElement.querySelector('.result-content') + private transformDisplayHTML(input: string): string { + // Replace lean with 

+        let result = input.replace(/lean\n/g, '
')
+        // Replace output info with 

+        result = result.replace(/output info\n/g, '
')
+        // Replace standalone  with 

+        result = result.replace(/<\/code>(?!<\/pre>)/g, '
')
+        // Replace {{#example_in ...}} and {{#example_out ...}} with placeholders
+        result = result.replace(/{{#example_in [\w/.]+}}/g, '[Example Input]')
+        result = result.replace(/{{#example_out [\w/.]+}}/g, '[Example Output]')
+        // Replace {{#example_decl ...}} with a placeholder
+        result = result.replace(/{{#example_decl [\w/.]+}}/g, '[Example Declaration]')
+        // Replace {{#example_eval ...}} with a placeholder
+        result = result.replace(/{{#example_eval [\w/.]+}}/g, '[Example Evaluation]')
+        // Remove any remaining newline character immediately after opening  tags
+        result = result.replace(/(\s*)\n/g, '')
+        return result
+    }
 
-            // Open the first result by default
-            if (index === 0) {
-                content?.classList.add('open')
-            }
+    private displayDocHit(element: HTMLElement, hit: DocHit) {
+        const modifiedHtmlContent = this.transformDisplayHTML(hit.displayHTML ?? '')
+        element.innerHTML = `
+            

+                
${hit.title}

+            

+            

+                View online
+                
${modifiedHtmlContent}

+            

+        `
+
+        // Add Lean syntax highlighting
+        element.querySelectorAll('code.language-lean').forEach(block => {
+            const code = block.innerHTML
+            block.innerHTML = code
+                .replace(/\b(def|fun|let|structure|where|match|with|Type|class)\b/g, '$1')
+                .replace(/\b(Nat|String|Bool|List|Option|Type)\b/g, '$1')
+                .replace(/(:=|->|→|←|↔|⟹|⟸|⟺)/g, '$1')
+        })
+
+        this.setupResultToggle(element)
+    }
+
+    private setupResultToggle(element: HTMLElement) {
+        const header = element.querySelector('.result-header')
+        const content = element.querySelector('.result-content')
 
-            header?.addEventListener('click', () => {
-                content?.classList.toggle('open')
-            })
+        header?.addEventListener('click', () => {
+            content?.classList.toggle('open')
         })
     }
 
diff --git a/vscode-lean4/moogleview/static/index.css b/vscode-lean4/moogleview/static/index.css
index c541fd07..0a43cc64 100644
--- a/vscode-lean4/moogleview/static/index.css
+++ b/vscode-lean4/moogleview/static/index.css
@@ -34,6 +34,8 @@
 .query-container {
     display: flex;
     align-items: center;
+    flex-wrap: wrap;
+    gap: 1rem;
 }
 
 .input-container {
@@ -124,10 +126,6 @@ h2 {
     display: block;
 }
 
-.result-content.open {
-    display: block;
-}
-
 .result-header h3 {
     margin: 0;
     font-size: 0.875rem;
@@ -196,3 +194,68 @@ vscode-link {
 .break_within {
     word-break: break-word;
 }
+
+.mode-select {
+    margin-left: 1rem;
+    display: flex;
+    align-items: center;
+}
+
+.toggle-switch {
+    display: flex;
+    align-items: center;
+    gap: 8px;
+}
+
+.toggle-text {
+    font-weight: normal;
+}
+
+.toggle-text.active {
+    font-weight: bold;
+}
+
+.switch {
+    position: relative;
+    display: inline-block;
+    width: 40px;
+    height: 20px;
+}
+
+.switch input {
+    opacity: 0;
+    width: 0;
+    height: 0;
+}
+
+.slider {
+    position: absolute;
+    cursor: pointer;
+    top: 0;
+    left: 0;
+    right: 0;
+    bottom: 0;
+    background-color: var(--vscode-button-background);
+    transition: 0.4s;
+    border-radius: 20px;
+}
+
+.slider:before {
+    position: absolute;
+    content: '';
+    height: 16px;
+    width: 16px;
+    left: 2px;
+    bottom: 2px;
+    background-color: var(--vscode-button-foreground);
+    transition: 0.4s;
+    border-radius: 50%;
+}
+
+input:checked + .slider {
+    background-color: var(--vscode-button-background);
+}
+
+input:checked + .slider:before {
+    transform: translateX(20px);
+}
diff --git a/vscode-lean4/moogleview/static/index.html b/vscode-lean4/moogleview/static/index.html
index 0064fe54..31426ae9 100644
--- a/vscode-lean4/moogleview/static/index.html
+++ b/vscode-lean4/moogleview/static/index.html
@@ -4,7 +4,18 @@
         

         
         
-        
+        
+    
+    

+        

+            Searching:
+            Theorems
+            
+            Docs
+        

     

     
 
@@ -18,7 +29,10 @@ 
 
 
Moogle — Find theorems, faster

 
-
Moogle is a semantic search engine designed to help you find theorems and definitions in Mathlib4 quickly. It is the result of a collaboration between Morph Labs and the Lean community.

+

+    Moogle is a semantic search engine designed to help you find theorems and definitions in Mathlib4 quickly. It is the
+    result of a collaboration between Morph Labs and the Lean community.
+

 
 
For a web version of this tool, visit moogle.ai.