Error on Hammer import - invalid option declaration 'lazyReduce.skipProof'

[barabbs]

I am encountering some issues in importing LeanHammer. I have a blank project, with lean-toolchain

leanprover/lean4:v4.20.0

and lakefile.lean

import Lake
open Lake DSL

package «LeanHammer» where
  -- add any additional package configuration options here

require Hammer from git "https://github.com/JOSHCLUNE/LeanHammer" @ "main"

Everything builds just fine running lake update and lake build Hammer, yet a simple lean file

import Hammer

raises the error LeanHammer.lean:1:0: invalid option declaration 'lazyReduce.skipProof', option already exists.

[barabbs]

I was able to give a better look to this today. Apparently the issue was that my lean file name contained dots... Changing it was enough to solve the issue.

The problem however sill arises for files that are not specified as @[default_target] in lakefile.lean