Improves formular (#1297)

* Improves formular

* adds back all nim releases

* removes unused `filterSatisfiableDeps`

* More improvements

* progress

src/nimblepkg/download.nim

@@ -495,7 +495,7 @@ proc downloadPkg*(url: string, verRange: VersionRange,
   except NimbleError: 
     #Continue with the download
     discard    
-  
+
   if subdir.len > 0:
     display("Downloading", "$1 using $2 (subdir is '$3')" %
                            [modUrl, downloadMethod, subdir],

src/nimblepkg/nimblesat.nim

@@ -62,6 +62,10 @@ type
   TaggedPackageVersions = object
     maxTaggedVersions: int # Maximum number of tags. When number changes, we invalidate the cache
     versions: seq[PackageMinimalInfo]
+
+  VersionAttempt = tuple[pkgName: string, version: Version]
+
+
 
 const TaggedVersionsFileName* = "tagged_versions.json"
 
@@ -169,70 +173,85 @@ proc toDepGraph*(versions: Table[string, PackageVersions]): DepGraph =
     result.packageToDependency[result.nodes[i].pkgName] = i
 
 proc toFormular*(g: var DepGraph): Form =
-# Key idea: use a SAT variable for every `Requirements` object, which are
-# shared.
   result = Form()
   var b = Builder()
   b.openOpr(AndForm)
-  # Assign a variable for each package version
+
+  # First pass: Assign variables and encode version selection constraints
   for p in mitems(g.nodes):
     if p.versions.len == 0: continue
     p.versions.sort(cmp)
-
-    for ver in mitems p.versions:
-      ver.v = VarId(result.idgen)
-      result.mapping[ver.v] = SatVarInfo(pkg: p.pkgName, version: ver.version, index: result.idgen)
-      inc result.idgen
-
-    # Encode the rule: for root packages, exactly one of its versions must be true
+
+    # Version selection constraint
     if p.isRoot:
       b.openOpr(ExactlyOneOfForm)
       for ver in mitems p.versions:
+        ver.v = VarId(result.idgen)
+        result.mapping[ver.v] = SatVarInfo(pkg: p.pkgName, version: ver.version, index: result.idgen)
         b.add(ver.v)
+        inc result.idgen
       b.closeOpr()
     else:
-      # For non-root packages, either one version is selected or none
-      b.openOpr(ZeroOrOneOfForm)
+      # For non-root packages, assign variables first
       for ver in mitems p.versions:
+        ver.v = VarId(result.idgen)
+        result.mapping[ver.v] = SatVarInfo(pkg: p.pkgName, version: ver.version, index: result.idgen)
+        inc result.idgen
+
+      # Then add ZeroOrOneOf constraint
+      b.openOpr(ZeroOrOneOfForm)
+      for ver in p.versions:
         b.add(ver.v)
       b.closeOpr()
 
-  # Model dependencies and their version constraints
+  # Second pass: Encode dependency implications
   for p in mitems(g.nodes):
     for ver in p.versions.mitems:
-      let eqVar = VarId(result.idgen)
-      # Mark the beginning position for a potential reset
-      let beforeDeps = b.getPatchPos()
-
-      inc result.idgen
-      var hasDeps = false
-
+      var allDepsCompatible = true
+
+      # First check if all dependencies can be satisfied
       for dep, q in items g.reqs[ver.req].deps:
-        let av = g.nodes[findDependencyForDep(g, dep)]
-        if av.versions.len == 0: continue
-
-        hasDeps = true
-        b.openOpr(ExactlyOneOfForm)  # Dependency must satisfy at least one of the version constraints
+        let depIdx = findDependencyForDep(g, dep)
+        if depIdx < 0: continue
+        let depNode = g.nodes[depIdx]
+
+        var hasCompatible = false
+        for depVer in depNode.versions:
+          if depVer.version.withinRange(q):
+            hasCompatible = true
+            break
+
+        if not hasCompatible:
+          allDepsCompatible = false
+          break
 
-        for avVer in av.versions:
-          if avVer.version.withinRange(q):
-            b.add(avVer.v)  # This version of the dependency satisfies the constraint
+      # If any dependency can't be satisfied, make this version unsatisfiable
+      if not allDepsCompatible:
+        b.addNegated(ver.v)
+        continue
 
-        b.closeOpr()
-
-      # If the package version is chosen and it has dependencies, enforce the dependencies' constraints
-      if hasDeps:
+      # Add implications for each dependency
+      for dep, q in items g.reqs[ver.req].deps:
+        let depIdx = findDependencyForDep(g, dep)
+        if depIdx < 0: continue
+        let depNode = g.nodes[depIdx]
+
+        var compatibleVersions: seq[VarId] = @[]
+        for depVer in depNode.versions:
+          if depVer.version.withinRange(q):
+            compatibleVersions.add(depVer.v)
+
+        # Add implication: if this version is selected, one of its compatible deps must be selected
         b.openOpr(OrForm)
-        b.addNegated(ver.v)  # If this package version is not chosen, skip the dependencies constraint
-        b.add(eqVar)  # Else, ensure the dependencies' constraints are met
+        b.addNegated(ver.v)  # not A
+        b.openOpr(OrForm)    # or (B1 or B2 or ...)
+        for compatVer in compatibleVersions:
+          b.add(compatVer)
+        b.closeOpr()
         b.closeOpr()
-
-      # If no dependencies were added, reset to beforeDeps to avoid empty or invalid operations
-      if not hasDeps:
-        b.resetToPatchPos(beforeDeps)
 
-  b.closeOpr()  # Close the main AndForm
-  result.f = toForm(b)  # Convert the builder to a formula
+  b.closeOpr()
+  result.f = toForm(b)
 
 proc toString(x: SatVarInfo): string =
   "(" & x.pkg & ", " & $x.version & ")"
@@ -256,6 +275,28 @@ proc getNodeByReqIdx(g: var DepGraph, reqIdx: int): Option[Dependency] =
       return some n
   none(Dependency)
 
+proc analyzeVersionSelection(g: DepGraph, f: Form, s: Solution): string =
+  result = "Version selection analysis:\n"
+
+  # Check which versions were selected
+  for node in g.nodes:
+    result.add &"\nPackage {node.pkgName}:"
+    var selectedVersion: Option[Version]
+    for ver in node.versions:
+      if s.isTrue(ver.v):
+        selectedVersion = some(ver.version)
+        result.add &"\n  Selected: {ver.version}"
+        # Show requirements for selected version
+        let reqs = g.reqs[ver.req].deps
+        result.add "\n  Requirements:"
+        for req in reqs:
+          result.add &"\n    {req.name} {req.ver}"
+    if selectedVersion.isNone:
+      result.add "\n  No version selected!"
+      result.add "\n  Available versions:"
+      for ver in node.versions:
+        result.add &"\n    {ver.version}"
+
 proc generateUnsatisfiableMessage(g: var DepGraph, f: Form, s: Solution): string =
   var conflicts: seq[string] = @[]
   for reqIdx, req in g.reqs:
@@ -332,34 +373,13 @@ proc findMinimalFailingSet*(g: var DepGraph): tuple[failingSet: seq[PkgTuple], o
 
   (minimalFailingSet, output)
 
-proc filterSatisfiableDeps(g: DepGraph, node: Dependency): seq[DependencyVersion] =
-  ## Returns a sequence of versions from the node that have satisfiable dependencies
-  result = @[]
-  for v in node.versions:
-    let reqs = g.reqs[v.req].deps
-    var hasUnsatisfiableDep = false
-    for req in reqs:
-      let depIdx = findDependencyForDep(g, req.name)
-      if depIdx >= 0:
-        var canSatisfy = false
-        for depVer in g.nodes[depIdx].versions:
-          if depVer.version.withinRange(req.ver):
-            canSatisfy = true
-            break
-        if not canSatisfy:
-          hasUnsatisfiableDep = true
-          break
-    if not hasUnsatisfiableDep:
-      result.add(v)
-
-const MaxSolverRetries = 100
-
 proc solve*(g: var DepGraph; f: Form, packages: var Table[string, Version], output: var string, 
-           retryCount = 0): bool =
+           triedVersions: var seq[VersionAttempt]): bool =
   let m = f.idgen
   var s = createSolution(m)
 
   if satisfiable(f.f, s):
+    # output.add analyzeVersionSelection(g, f, s)
     for n in mitems g.nodes:
       if n.isRoot: n.active = true
     for i in 0 ..< m:
@@ -379,29 +399,42 @@ proc solve*(g: var DepGraph; f: Form, packages: var Table[string, Version], outp
           output.add &"item.pkg  [ ]  {toString item} \n"
     return true
   else:
+    output.add "\nFailed to find satisfiable solution:\n"
+    output.add analyzeVersionSelection(g, f, s)
     let (failingSet, errorMsg) = findMinimalFailingSet(g)
-    if retryCount >= MaxSolverRetries:
-      output = &"Max retry attempts ({MaxSolverRetries}) exceeded while trying to resolve dependencies \n"
-      output.add errorMsg
-      return false
-
     if failingSet.len > 0:
       var newGraph = g
+
+      # Try each failing package
       for pkg in failingSet:
         let idx = findDependencyForDep(newGraph, pkg.name)
         if idx >= 0:
-          # echo "Retry #", retryCount + 1, ": Checking package ", pkg.name, " version ", pkg.ver
-          let newVersions = filterSatisfiableDeps(newGraph, newGraph.nodes[idx])
-          if newVersions.len > 0 and newVersions != newGraph.nodes[idx].versions:
-            newGraph.nodes[idx].versions = newVersions
-            let newForm = toFormular(newGraph)
-            return solve(newGraph, newForm, packages, output, retryCount + 1)
+          let originalVersions = newGraph.nodes[idx].versions
+          # Try each version once, from newest to oldest
+          for ver in originalVersions:
+            let attempt = (pkgName: pkg.name, version: ver.version)
+            if attempt notin triedVersions:
+              triedVersions.add(attempt)
+              # echo "Trying package ", pkg.name, " version ", ver.version
+              newGraph.nodes[idx].versions = @[ver]  # Try just this version
+              let newForm = toFormular(newGraph)
+              if solve(newGraph, newForm, packages, output, triedVersions):
+                return true
+          # Restore original versions if no solution found
+          newGraph.nodes[idx].versions = originalVersions
 
-      output = errorMsg
+      output.add "\n\nFinal error message:\n"  # Add a separator
+      output.add errorMsg
     else:
-      output = generateUnsatisfiableMessage(g, f, s)
+      output.add "\n\nFinal error message:\n"  # Add a separator
+      output.add generateUnsatisfiableMessage(g, f, s)
     false
 
+
+proc solve*(g: var DepGraph; f: Form, packages: var Table[string, Version], output: var string): bool =
+  var triedVersions = newSeq[VersionAttempt]()
+  solve(g, f, packages, output, triedVersions)
+
 proc collectReverseDependencies*(targetPkgName: string, graph: DepGraph): seq[(string, Version)] =
   for node in graph.nodes:
     for version in node.versions:
@@ -427,7 +460,8 @@ proc getSolvedPackages*(pkgVersionTable: Table[string, PackageVersions], output:
 
   let form = toFormular(graph)
   var packages = initTable[string, Version]()
-  discard solve(graph, form, packages, output)
+  var triedVersions: seq[VersionAttempt] = @[]
+  discard solve(graph, form, packages, output, triedVersions)
 
   for pkg, ver in packages:
     let nodeIdx = graph.packageToDependency[pkg]
@@ -457,7 +491,7 @@ proc downloadPkInfoForPv*(pv: PkgTuple, options: Options): PackageInfo  =
   downloadPkgFromUrl(pv, options)[0].dir.getPkgInfo(options)
 
 proc getAllNimReleases(options: Options): seq[PackageMinimalInfo] =
-  let releases = getOfficialReleases(options)
+  let releases = getOfficialReleases(options)  
   for release in releases:
     result.add PackageMinimalInfo(name: "nim", version: release)
 
@@ -635,3 +669,4 @@ proc getPackageInfo*(name: string, pkgs: seq[PackageInfo], version: Option[Versi
             return some pkg
         else: #No version passed over first match
           return some pkg
+

src/nimblepkg/options.nim

@@ -754,7 +754,7 @@ proc initOptions*(): Options =
     noColor: not isatty(stdout),
     startDir: getCurrentDir(),
     nimBinariesDir: getHomeDir() / ".nimble" / "nimbinaries", 
-    maxTaggedVersions: 2 
+    maxTaggedVersions: 4
   )
 
 proc handleUnknownFlags(options: var Options) =

tests/libp2pconflict/libp2pconflict.nimble

@@ -0,0 +1,16 @@
+# Package
+
+version       = "0.1.0"
+author        = "jmgomez"
+description   = "A new awesome nimble package"
+license       = "MIT"
+srcDir        = "src"
+
+
+# Dependencies
+
+requires(
+  "nim >= 1.6.12",
+  "libp2p",
+  "https://github.com/status-im/nim-quic.git#8a97eeeb803614bce2eb0e4696127d813fea7526"
+)

tests/libp2pconflict/src/libp2pconflict.nim

@@ -0,0 +1,7 @@
+# This is just an example to get you started. A typical library package
+# exports the main API in this file. Note that you cannot rename this file
+# but you can remove it if you wish.
+
+proc add*(x, y: int): int =
+  ## Adds two numbers together.
+  return x + y

tests/libp2pconflict/src/libp2pconflict/submodule.nim

@@ -0,0 +1,12 @@
+# This is just an example to get you started. Users of your library will
+# import this file by writing ``import libp2pconflict/submodule``. Feel free to rename or
+# remove this file altogether. You may create additional modules alongside
+# this file as required.
+
+type
+  Submodule* = object
+    name*: string
+
+proc initSubmodule*(): Submodule =
+  ## Initialises a new ``Submodule`` object.
+  Submodule(name: "Anonymous")

tests/libp2pconflict/tests/test1.nim

@@ -0,0 +1,12 @@
+# This is just an example to get you started. You may wish to put all of your
+# tests into a single file, or separate them into multiple `test1`, `test2`
+# etc. files (better names are recommended, just make sure the name starts with
+# the letter 't').
+#
+# To run these tests, simply execute `nimble test`.
+
+import unittest
+
+import libp2pconflict
+test "can add":
+  check add(5, 5) == 10

tests/tsat.nim

@@ -394,4 +394,19 @@ suite "SAT solver":
     cd "oldnimble": #0.16.2
       removeDir("nimbledeps")
       let (_, exitCode) = execNimbleYes("install", "-l")
-      check exitCode == QuitSuccess
+      check exitCode == QuitSuccess
+
+  test "should be able to fallback to a previous version of a dependency when unsatisfable (complex case)":
+    #There is an issue with 
+    #[
+      "libp2p",
+      "https://github.com/status-im/nim-quic.git#8a97eeeb803614bce2eb0e4696127d813fea7526"
+    
+    Where libp2p needs to be set to an older version (15) as the constraints from nim-quic are incompatible with the 
+    constraints from libp2p > 15.
+    
+    ]#
+    cd "libp2pconflict": #0.16.2
+      removeDir("nimbledeps")
+      let (_, exitCode) = execNimbleYes("install", "-l")
+      check exitCode == QuitSuccess