unknown module prefix 'tactic'

Stream: lean4

[Kajani Kaunda]

This following code does not work on both my VS Code + LEan4 setup and https://live.lean-lang.org/

import tactic
def hello := "hello!"
#eval hello

However there is file called tactic.lean in the following folder:
C:\DATA\LEAN\spgf\.lake\packages\mathlib\Mathlib

The error i am getting is:

unknown module prefix 'tactic'
No directory 'tactic' or file 'tactic.olean' in the search path entries:

followed by a list of folders.

is it an environment problem, a lean version problem (3/4), or am I mixing lean 3 constructs in lean 4, or a worse sin ...

[Damiano Testa]

Mathlib.Tactic?

[Kajani Kaunda]

Damiano Testa said:

Mathlib.Tactic?

not. lower case 't'.
But there is a folder called Mathlib.Tactic. Are they the same?

[Eric Wieser]

You are writing Lean 3 code but running it with lean 4

[Kajani Kaunda]

Eric Wieser said:

You are writing Lean 3 code but running it with lean 4

Ouch!

[Kajani Kaunda]

So what is the equivalent lean 4 code?

[Patrick Massot]

You don’t need any import for this code, the last two lines should work.

[Kajani Kaunda]

Kajani Kaunda said:

So what is the equivalent lean 4 code?

Thank you.

[Kajani Kaunda]

Patrick Massot said:

You don’t need any import for this code, the last two lines should work.

Noted.

Patrick Massot said:

You don’t need any import for this code, the last two lines should work.

Thank you.