mathlib4/MathlibTest/ForbiddenModuleNames.lean at master · Stars1233/mathlib4 · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
module

import all Mathlib.Tactic.Linter.TextBased

/-!
# Unit tests for the module name compatibility checks in the text-based linter
-/

open Lean.Linter Mathlib.Linter.TextBased

/-- Some unit tests for `modulesOSForbidden` -/
meta def testModulesOSForbidden : IO Unit := do
  -- Explicitly enable the linter, although it is enabled by default.
  let opts : LinterOptions := {
    toOptions := linter.modulesUpperCamelCase.set {} true
    linterSets := {}
  }

  assert!((← modulesOSForbidden opts #[]) == 0)
  assert!((← modulesOSForbidden opts #[`Mathlib.Aux.Foo, `Mathlib.Algebra.Con]) == 2)
  assert!((← modulesOSForbidden opts #[`Mathlib.Foo.Bar, `Aux.Algebra.Con.Bar]) == 1)
  assert!((← modulesOSForbidden opts #[`Com1.prn.Aux, `LPT.Aux]) == 2)
  assert!((← modulesOSForbidden opts #[`Mathlib.Foo.«Foo*»]) == 1)
  assert!((← modulesOSForbidden opts #[`Mathlib.«B>ar<»]) == 1)
  assert!((← modulesOSForbidden opts #[`Mathlib.«Bar!»]) == 1)
  assert!((← modulesOSForbidden opts #[`Mathlib.«Qu<x!!»]) == 1)
  assert!((← modulesOSForbidden opts #[`Mathlib.«Ba dname»]) == 1)
  assert!((← modulesOSForbidden opts #[`Mathlib.«Bar dname»]) == 1)
  assert!((← modulesOSForbidden opts #[`Mathlib.«Bar
dname»]) == 1)

/--
info: error: module name 'Mathlib.Aux.Foo' contains component '[Aux]', which is forbidden in Windows filenames.
error: module name 'Mathlib.Algebra.Con' contains component '[Con]', which is forbidden in Windows filenames.
error: module name 'Aux.Algebra.Con.Bar' contains components '[Aux, Con]', which are forbidden in Windows filenames.
error: module name 'Com1.prn.Aux' contains components '[Com1, prn, Aux]', which are forbidden in Windows filenames.
error: module name 'LPT.Aux' contains component '[Aux]', which is forbidden in Windows filenames.
error: module name 'Mathlib.Foo.«Foo*»' contains character '[*]', which is forbidden in Windows filenames.
error: module name 'Mathlib.«B>ar<»' contains characters '[>, <]', which are forbidden in Windows filenames.
error: module name 'Mathlib.Bar!' contains forbidden character '!'
error: module name 'Mathlib.«Qu<x!!»' contains forbidden character '!'
error: module name 'Mathlib.«Qu<x!!»' contains character '[<]', which is forbidden in Windows filenames.
error: module name 'Mathlib.«Ba dname»' contains a whitespace character
error: module name 'Mathlib.«Bar dname»' contains a whitespace character
error: module name 'Mathlib.«Bar
dname»' contains a whitespace character
-/
#guard_msgs in
#eval testModulesOSForbidden