Merge pull request #107 from lean-dojo/peiyang

Incorporate recent commits

.dockerignore

@@ -3,5 +3,5 @@
 tmp
 .lake
 clang+llvm*
-python/__pycache__
+**/__pycache__
 */.DS_Store

.gitignore

@@ -1,5 +1,5 @@
 .lake
 .vscode
 *.olean
-python/__pycache__
+**/__pycache__
 */.DS_Store

LeanCopilot/Tactics.lean

@@ -80,9 +80,9 @@ private def annotatePremise (pi : PremiseInfo) : MetaM String := do
     let info ← getConstInfo declName
     let premise_type ← Meta.ppExpr info.type
     let some doc_str ← findDocString? (← getEnv) declName
-      | return s!"\n{pi.name} : {premise_type}"
-    return s!"\n{pi.name} : {premise_type}\n```doc\n{doc_str}\n```"
-  catch _ => return s!"\n{pi.name} needs to be imported from {pi.path}.\n```code\n{pi.code}\n```"
+      | return s!"{pi.name} : {premise_type}\n"
+    return s!"{pi.name} : {premise_type}\n```doc\n{doc_str}\n```\n"
+  catch _ => return s!"{pi.name} needs to be imported from `{pi.path}`.\n```code\n{pi.code}\n```\n"
 
 
 /--

LeanCopilotTests/ProofSearch.lean

@@ -33,5 +33,4 @@ set_option trace.aesop true
 
 
 example (a b c : Nat) : a + b + c = c + b + a := by
-  try aesop? (config := { maxRuleApplications := 2 })
-  try sorry
+  aesop? (config := { maxRuleApplications := 2 })