let to_name = String.concat "_"
let to_dir  = String.concat "/"
let prefix  = "coq-pkgs"

(* Default FS list *)
let plugin_list =
  [ ["Coq"; "ltac"]
  ; ["Coq"; "syntax"]
  ; ["Coq"; "decl_mode"]
  ; ["Coq"; "cc"]
  ; ["Coq"; "firstorder"]
  ; ["Coq"; "setoid_ring"]
  ; ["Coq"; "extraction"]
  ; ["Coq"; "funind"]
  ; ["Coq"; "quote"]

  ; ["Coq"; "fourier"]
  ; ["Coq"; "omega"]
  ; ["Coq"; "micromega"]
  ; ["Coq"; "romega"]
  ; ["Coq"; "nsatz"]
  ; ["Coq"; "ssrmatching"]
  ; ["Coq"; "ssr"]
  ]

let coq_theory_list =
  [ ["Coq"; "Init"]
  ; ["Coq"; "Unicode"]
  ; ["Coq"; "Bool"]
  ; ["Coq"; "Logic"]
  ; ["Coq"; "Program"]
  ; ["Coq"; "Classes"]
  ; ["Coq"; "Structures"]
  ; ["Coq"; "Relations"]
  ; ["Coq"; "Setoids"]
  ; ["Coq"; "Arith"]
  ; ["Coq"; "PArith"]
  ; ["Coq"; "NArith"]
  ; ["Coq"; "ZArith"]
  ; ["Coq"; "QArith"]
  ; ["Coq"; "Lists"]
  ; ["Coq"; "Vectors"]
  ; ["Coq"; "Reals"]
  ; ["Coq"; "Sets"]
  ; ["Coq"; "FSets"]
  ; ["Coq"; "MSets"]
  ; ["Coq"; "Sorting"]
  ; ["Coq"; "Wellfounded"]
  ; ["Coq"; "Strings"]

  ; ["Coq"; "Numbers"]
  ; ["Coq"; "Numbers"; "NatInt"]
  ; ["Coq"; "Numbers"; "Natural"; "Abstract"]
  ; ["Coq"; "Numbers"; "Natural"; "Peano"]
  ; ["Coq"; "Numbers"; "Integer"; "Abstract"]
  ]

(* Packages: name, deps, modules *)

let pkgs : (string * string list * string list list) list=
  [ "init", [],
    [ ["Coq"; "ltac"]
    ; ["Coq"; "syntax"]
    ; ["Coq"; "decl_mode"]
    ; ["Coq"; "cc"]
    ; ["Coq"; "firstorder"]
    ; ["Coq"; "extraction"]
    ; ["Coq"; "funind"]
    ; ["Coq"; "quote"]
    ; ["Coq"; "Init"]
    ; ["Coq"; "Bool"]
    ; ["Coq"; "Unicode"]
    ; ["Coq"; "ssrmatching"]
    ; ["Coq"; "ssr"]
    ; ["mathcomp"; "ssreflect"]
    ]
  ; "math-comp", [],
    [ ["mathcomp"; "algebra"]
    ; ["mathcomp"; "fingroup"]
    ; ["mathcomp"; "solvable"]
    ; ["mathcomp"; "field"]
    ; ["mathcomp"; "character"]
    ; ["mathcomp"; "odd_order"]
    ]
  ; "coq-base", [],
    [ ["Coq"; "Logic"]
    ; ["Coq"; "Program"]
    ; ["Coq"; "Classes"]
    ; ["Coq"; "Structures"]
    ; ["Coq"; "Relations"]
    ; ["Coq"; "Setoids"]
    ; ["Coq"; "Lists"]
    ; ["Coq"; "Vectors"]
    ; ["Coq"; "Sets"]
    ; ["Coq"; "Sorting"]
    ; ["Coq"; "FSets"]
    ; ["Coq"; "MSets"]
    ; ["Coq"; "Wellfounded"]
    ; ["Coq"; "Strings"]
    ]
  ; "coq-arith", ["coq-base"],
    [ ["Coq"; "setoid_ring"]
    ; ["Coq"; "Arith"]
    ; ["Coq"; "NArith"]
    ; ["Coq"; "PArith"]
    ; ["Coq"; "ZArith"]
    ; ["Coq"; "QArith"]
    ; ["Coq"; "Numbers"]
    ; ["Coq"; "Numbers"; "NatInt"]
    ; ["Coq"; "Numbers"; "Natural"; "Abstract"]
    ; ["Coq"; "Numbers"; "Natural"; "Peano"]
    ; ["Coq"; "Numbers"; "Integer"; "Abstract"]
    ]
  ; "mtac", ["coq-arith"],
    [ ["Mtac"]
    ]

  ; "coq-reals", ["coq-arith"],
    [ ["Coq"; "fourier"]
    ; ["Coq"; "omega"]
    ; ["Coq"; "micromega"]
    ; ["Coq"; "nsatz"]
    ; ["Coq"; "Reals"] ]

  ; "coquelicot", ["coq-reals"],
    [ [ "Coquelicot" ] ]

  ; "flocq", ["coq-reals"],
    [ [ "Coq"   ; "romega"]
    ; [ "Flocq" ; "Core" ]
    ; [ "Flocq" ; "Appli" ]
    ; [ "Flocq" ; "Calc" ]
    ; [ "Flocq" ; "Translate" ]
    ; [ "Flocq" ; "Prop" ] ]

  ; "tlc", ["coq-reals"],
    [ ["TLC"] ]
  ; "sf", ["coq-reals"],
    [ ["SF"] ]
  ; "cpdt", ["coq-reals"],
    [ ["Cpdt"] ]

  ; "color", [ "coq-reals"],
    [ ["CoLoR" ; "Filter"]
    ; ["CoLoR" ; "RPO"]
    ; ["CoLoR" ; "Coccinelle"]
    ; ["CoLoR" ; "Coccinelle" ; "list_extensions"]
    ; ["CoLoR" ; "Coccinelle" ; "term_orderings"]
    ; ["CoLoR" ; "Coccinelle" ; "basis"]
    ; ["CoLoR" ; "Coccinelle" ; "examples"]
    ; ["CoLoR" ; "Coccinelle" ; "examples" ; "cime_trace"]
    ; ["CoLoR" ; "Coccinelle" ; "ac_matching"]
    ; ["CoLoR" ; "Coccinelle" ; "term_algebra"]
    ; ["CoLoR" ; "Coccinelle" ; "unification"]
    ; ["CoLoR" ; "NonTermin"]
    ; ["CoLoR" ; "Term"]
    ; ["CoLoR" ; "Term" ; "Lambda"]
    ; ["CoLoR" ; "Term" ; "SimpleType"]
    ; ["CoLoR" ; "Term" ; "String"]
    ; ["CoLoR" ; "Term" ; "Varyadic"]
    ; ["CoLoR" ; "Term" ; "WithArity"]
    ; ["CoLoR" ; "HORPO"]
    ; ["CoLoR" ; "ProofChecker"]
    ; ["CoLoR" ; "MatrixInt"]
    ; ["CoLoR" ; "SemLab"]
    ; ["CoLoR" ; "Conversion"]
    ; ["CoLoR" ; "DP"]
    ; ["CoLoR" ; "Util"]
    ; ["CoLoR" ; "Util" ; "Multiset"]
    ; ["CoLoR" ; "Util" ; "Vector"]
    ; ["CoLoR" ; "Util" ; "Pair"]
    ; ["CoLoR" ; "Util" ; "FSet"]
    ; ["CoLoR" ; "Util" ; "Integer"]
    ; ["CoLoR" ; "Util" ; "FMap"]
    ; ["CoLoR" ; "Util" ; "Matrix"]
    ; ["CoLoR" ; "Util" ; "Logic"]
    ; ["CoLoR" ; "Util" ; "Polynom"]
    ; ["CoLoR" ; "Util" ; "Option"]
    ; ["CoLoR" ; "Util" ; "FGraph"]
    ; ["CoLoR" ; "Util" ; "Function"]
    ; ["CoLoR" ; "Util" ; "List"]
    ; ["CoLoR" ; "Util" ; "Relation"]
    ; ["CoLoR" ; "Util" ; "Bool"]
    ; ["CoLoR" ; "Util" ; "Nat"]
    ; ["CoLoR" ; "Util" ; "Set"]
    ; ["CoLoR" ; "Util" ; "Algebra"]
    ; ["CoLoR" ; "PolyInt"]
    ; ["CoLoR" ; "SubtermCrit"]
    ; ["CoLoR" ; "MPO"]
    ; ["CoLoR" ; "MannaNess"]
    ]

  ; "dsp", ["math-comp"],
    [ ["Dsp"] ]

  ; "relalg", ["coq-arith"],
    [ ["RelationAlgebra"] ]

  ; "hott-init", [],
    [ ["Coq"; "syntax"]
    ; ["Coq"; "Init"]
    ; ["Coq"; "Bool"]
    ; ["Coq"; "Program"]
    ; ["Coq"; "Unicode"]
    ]

  ; "hott", ["hott-init"],

    [ ["HoTT"]
    ; ["HoTT" ; "Algebra"]
    ; ["HoTT" ; "Basics"]
    ; ["HoTT" ; "categories"]
    ; ["HoTT" ; "categories"; "Adjoint"]
    ; ["HoTT" ; "categories"; "Adjoint"; "Composition"]
    ; ["HoTT" ; "categories"; "Adjoint"; "Functorial"]
    ; ["HoTT" ; "categories"; "Adjoint"; "UniversalMorphisms"]
    ; ["HoTT" ; "categories"; "Cat"]
    ; ["HoTT" ; "categories"; "Category"]
    ; ["HoTT" ; "categories"; "Category"; "Sigma"]
    ; ["HoTT" ; "categories"; "Category"; "Subcategory"]
    ; ["HoTT" ; "categories"; "CategoryOfSections"]
    ; ["HoTT" ; "categories"; "Comma"]
    ; ["HoTT" ; "categories"; "ExponentialLaws"]
    ; ["HoTT" ; "categories"; "ExponentialLaws"; "Law1"]
    ; ["HoTT" ; "categories"; "ExponentialLaws"; "Law2"]
    ; ["HoTT" ; "categories"; "ExponentialLaws"; "Law3"]
    ; ["HoTT" ; "categories"; "ExponentialLaws"; "Law4"]
    ; ["HoTT" ; "categories"; "Functor"]
    ; ["HoTT" ; "categories"; "Functor"; "Composition"]
    ; ["HoTT" ; "categories"; "Functor"; "Composition"; "Functorial"]
    ; ["HoTT" ; "categories"; "Functor"; "Prod"]
    ; ["HoTT" ; "categories"; "Functor"; "Pointwise"]
    ; ["HoTT" ; "categories"; "FunctorCategory"]
    ; ["HoTT" ; "categories"; "Grothendieck"]
    ; ["HoTT" ; "categories"; "Grothendieck"; "ToSet"]
    ; ["HoTT" ; "categories"; "GroupoidCategory"]
    ; ["HoTT" ; "categories"; "InitialTerminalCategory"]
    ; ["HoTT" ; "categories"; "KanExtensions"]
    ; ["HoTT" ; "categories"; "LaxComma"]
    ; ["HoTT" ; "categories"; "Limits"]
    ; ["HoTT" ; "categories"; "NaturalTransformation"]
    ; ["HoTT" ; "categories"; "NaturalTransformation"; "Composition"]
    ; ["HoTT" ; "categories"; "Profunctor"]
    ; ["HoTT" ; "categories"; "Pseudofunctor"]
    ; ["HoTT" ; "categories"; "PseudonaturalTransformation"]
    ; ["HoTT" ; "categories"; "SetCategory"]
    ; ["HoTT" ; "categories"; "SetCategory"; "Functors"]
    ; ["HoTT" ; "categories"; "Structure"]
    ; ["HoTT" ; "Comodalities"]
    ; ["HoTT" ; "HIT"]
    ; ["HoTT" ; "Modalities"]
    ; ["HoTT" ; "Spaces"]
    ; ["HoTT" ; "Tactics"]
    ; ["HoTT" ; "Types"] ]

  ; "unimath", [ ],

    [ ["UniMath"]
    ; ["UniMath" ; "CategoryTheory" ]
    ; ["UniMath" ; "CategoryTheory" ; "limits" ]
    ; ["UniMath" ; "CategoryTheory" ; "colimits" ]
    ; ["UniMath" ; "PAdics" ]
    ; ["UniMath" ; "Ktheory" ]
    ; ["UniMath" ; "Tactics" ]
    ; ["UniMath" ; "SubstitutionSystems" ]
    ; ["UniMath" ; "Foundations" ]
    ; ["UniMath" ; "Foundations" ; "Basics" ]
    ; ["UniMath" ; "Foundations" ; "Combinatorics" ]
    ; ["UniMath" ; "Foundations" ; "Algebra" ]
    ; ["UniMath" ; "Foundations" ; "NumberSystems" ]
    ; ["UniMath" ; "Dedekind" ]
    ]

  ; "peacoq", [ "init" ],
    [ ["PeaCoq"] ]

  ; "extlib", [ "coq-reals" ],
    [ ["ExtLib"]
    ; ["ExtLib" ; "Core" ]
    ; ["ExtLib" ; "Data" ]
    ; ["ExtLib" ; "Data"; "Eq" ]
    ; ["ExtLib" ; "Data"; "Graph" ]
    ; ["ExtLib" ; "Data"; "Map" ]
    ; ["ExtLib" ; "Data"; "Monads" ]
    ; ["ExtLib" ; "Data"; "Set" ]
    ; ["ExtLib" ; "Generic" ]
    ; ["ExtLib" ; "Programming" ]
    ; ["ExtLib" ; "Recur" ]
    ; ["ExtLib" ; "Relations" ]
    ; ["ExtLib" ; "Structures" ]
    ; ["ExtLib" ; "Tactics" ]
    ]

  ; "plugin-utils", [ ],
    [ ["PluginUtils"] ]

  ; "mirrorcore", [ "plugin-utils"; "extlib" ],
    [ ["MirrorCore"]
    ; ["MirrorCore" ; "Lambda" ]
    ; ["MirrorCore" ; "Lambda"; "Rewrite" ]
    ; ["MirrorCore" ; "MTypes" ]
    ; ["MirrorCore" ; "Reify" ]
    ; ["MirrorCore" ; "RTac" ]
    ; ["MirrorCore" ; "Subst" ]
    ; ["MirrorCore" ; "syms" ]
    ; ["MirrorCore" ; "Util" ]
    ; ["MirrorCore" ; "Views" ]

    ; ["McExamples" ; "Cancel" ]
    ]

  ; "stdpp", [ "coq-reals" ],
    [ [ "stdpp" ] ]

  ; "iris", [ "stdpp" ],
    [ [ "iris" ]
    ; [ "iris" ; "algebra" ]
    ; [ "iris" ; "base_logic" ]
    ; [ "iris" ; "base_logic" ; "lib" ]
    ; [ "iris" ; "heap_lang" ]
    ; [ "iris" ; "base_lang" ; "lib" ]
    ; [ "iris" ; "program_logic" ]
    ; [ "iris" ; "proofmode" ]
    ; [ "iris" ; "tests" ]
    ]

  ; "elpi", [ ],
    [ [ "elpi" ]
    ; [ "elpi" ; "ltac" ]
    ; [ "elpi" ; "test" ]
    ; [ "elpi" ; "tutorial" ]
    ; [ "elpi" ; "derive" ]
    ]

  ; "equations", [ "coq-reals" ],
    [ [ "Equations" ]
    ]

  ; "ltac2", [ ],
    [ [ "Ltac2" ]
    ]
  ]