# @author ygw
#
# Public DeepSeek Harness bundle layer. The DSH profile that installs this package
# resolves the package name below to the `./dsh` export in package.json.

- insert:
    - id: lean4-harness-plugin
      name: 'lean4-harness-plugin/dsh'
      config:
        # Keep the guard aligned with lean/lakefile.lean's local Mathlib path.
        # @author ygw
        mathlibRoot: 'D:/mathlib4'
        requestTimeoutMs: 600000
        buildTimeoutMs: 600000
        prewarm: false
        prewarmSource: |
          import Mathlib.Data.Nat.Basic