fastest way to copy module name of the current file?

Stream: lean4

[Junyan Xu]

What's the easiest way to copy the module name of the current file? Currently I have three ideas (mostly I've only done 1 and 2):

1. copy the file name (right click on the tab in VSCode and select "Copy Relative Path"), remove the trailing .lean and replace all / by ..

2. maybe a module with a similar name exists among the imports of the file. Copy that and manually modify the last few bits.

3. search a declaration in the file in the online docs and copy the title of the page.

Un-#xy: In Lean 3 if I want to build a file I can just copy the file name and run lean <file_name>, but in Lean 4 lake build demands a module name not a file name, hence the question. Of course I can now "Restart File" in VSCode, but build progress is not shown in the infoview and I can't estimate how long it would take. Maybe we could make lake build automatically turn a file name into a module name?

[Damiano Testa]

Does lake env lean <file_path> do what you want?

[Damiano Testa]

(btw, for other reasons, I also have a command-line function that converts a file path to a module name, i.e. removes trailing .lean and replaces / with ..)

[Scott Morrison]

The lean4-cli library has a special parser for module names that takes either variant.

[Scott Morrison]

If you want to open an issue, and tag it with lake, we might eventually get there. I agree it would be nice!

[Damiano Testa]

In the meantime, if the paths that you copy begin with Mathlib, you can use this "Try this" suggestion :smile:

import Std.Tactic.TryThis

open Lean Elab Command
namespace importMe

syntax importPath := sepBy1(ident, "/")
syntax "Mathlib" "/" (ppSpace colGt importPath) : command

/--  A syntax that allows strings to be printed without surrounding them by guillemets `«...»`. -/
declare_syntax_cat write_me_output_stx

syntax "lake build " ident : write_me_output_stx

def toSuggestion (root : String) (parts : Array (TSyntax `ident)) :
    TermElabM (TSyntax `write_me_output_stx) := do
  let strParts := parts.map fun s ↦ s.getId.toString (escape := false)
  -- Rebuild the path and interpret it as a `System.FilePath`.
  let path : System.FilePath := root ++ "/" ++ String.intercalate "/" strParts.toList
  let impS ← Lean.moduleNameOfFileName path none
  `(write_me_output_stx| lake build $(mkIdent impS))

elab_rules : command
| `(command| Mathlib/ $[$parts]/*) => liftTermElabM do
  let stx ← getRef
  let replacement ← toSuggestion "Mathlib" parts
  Std.Tactic.TryThis.addSuggestion stx replacement (origSpan? := stx)

end importMe

Mathlib/Data/Nat/Basic.lean
-- Try this: lake build Mathlib.Data.Nat.Basic

[Damiano Testa]

So you copy-paste the relative file/path.lean in a lean file and you get the Try this suggestion for lake build module.name.

[Junyan Xu]

Damiano Testa said:

In the meantime, if the paths that you copy begin with Mathlib, you can use this "Try this" suggestion :smile:

Thanks! This works. lake env lean <file_path> apparently doesn't show progress, i.e. how many files are built and how many need to be built in total.

[Damiano Testa]

@Junyan Xu I do not know what the difference between the two commands lean module.name and lake env lean file/path.lean is (and would be curious to know what it is!).

Anyway, as Scott said, maybe there should be better support for the difference between module names and file names. Currently, for me a combination of the command above and the commandline replacements have been convenient.

[Damiano Testa]

To remove potential mystery about the commandline stuff: I added this (bash) function to my environment

lb () {
  local var="${1//\//.}"      # replace `/` with `.`
  lake build "${var%.lean}"   # do `lake build` on the replacement, after removing trailing `.lean`
}

so that typing lb file/path.lean means lake build module.name.

This is just working on strings, so it actually also works with file/paths that do not begin with Mathlib as well.

[Marc Huisinga]

See also searchModuleNameOfFileName. The important bit is that you need to know the search path.

[Yaël Dillies]

Junyan Xu said:

Maybe we could make lake build automatically turn a file name into a module name?

I have the same request for cache!

[Mario Carneiro]

For lake build, this is lean4#2756. I don't think there are any major blockers but it doesn't seem to be a high priority. (As usual, you should upvote it if you want to raise the priority.)

[Junyan Xu]

I'm reminded of a side question I had by your extra feature request:

Also, it would be good if this works even for files outside the module tree, such as lake build test/ring.lean for mathlib4. I am not sure there is any current option which this is equivalent to, but what it should do is build all the dependencies of the file (as specified in the import lines) and then call the equivalent of lake env lean test/ring.lean.

With Lean 3 I used to be able to create a new file in VSCode without saving it to the disk, and as I type imports and declarations into it, Lean would immediately react to them (assuming I've opened a mathlib workspace). This is convenient when I want to investigate some #mwe and don't want to save anything to the git repo and risk mistakenly committing the file, and VSCode does a good job restoring unsaved files across sessions.

However with Lean 4 this no longer works: if I don't save it into the git repo (or maybe the directory governed by lakefile is more precise?) then Lean will just ignore it, so I tend to use the web editor for such temporary Lean coding now that it is up and functioning. Does the web editor secretly saves the file somewhere in a directory?

[Scott Morrison]

Yaël Dillies said:

Junyan Xu said:

Maybe we could make lake build automatically turn a file name into a module name?

I have the same request for cache!

This one you can implement yourself: cache is all in Mathlib.