Add csdp support for Micromega tactics in Coq.

[roconnor]

No description provided.

[roconnor]

The http://www.coin-or.org/ website is currently down for maintenance. That is why the travis-ci is failing. I'll wait for the website to return before I push this change.

[roconnor]

Now travis-ci is failing because the test is too large. I successfully ran the following command on my desktop, so I think it is fine.

nix-build -A coqPackages.contribs.RelationAlgebra -A coqPackages.contribs.Continuations -A coqPackages.coqExtLib -A compcert -A coqPackages.contribs.TortoiseHareAlgorithm -A coqPackages.contribs.EulerFormula -A coqPackages.contribs.TarskiGeometry -A coqPackages.contribs.CoRN -A coqPackages.ssreflect -A coqPackages.contribs.Maths -A coqPackages_8_5.coq -A coqPackages.contribs.HigmanS -A coqPackages.unimath -A coqPackages.contribs.GraphBasics -A coqPackages.contribs.Chinese -A coqPackages.contribs.Subst -A coqPackages.domains -A coqPackages.contribs.FiringSquad -A coqPackages.contribs.CoursDeCoq -A coqPackages.contribs.Ramsey -A coqPackages.contribs.CanonBDDs -A coqPackages.contribs.WeakUpTo -A coqPackages.contribs.Streams -A coqPackages.contribs.DomainTheory -A coqPackages.paco -A coqPackages.contribs.IPC -A coqPackages.contribs.RelationExtraction -A coqPackages.contribs.RailroadCrossing -A why3 -A coqPackages.contribs.RecursiveDefinition -A coqPackages.contribs.Angles -A coqPackages.QuickChick -A coqPackages.contribs.ModRed -A coqPackages.contribs.Pocklington -A coqPackages.contribs.Groups -A coqPackages.contribs.Topology -A coqPackages.contribs.PAutomata -A coqPackages.contribs.RegExp -A coqPackages.contribs.IEEE754 -A coqPackages.contribs.CTLTCTL -A coqPackages.bedrock -A coqPackages.contribs.RSA -A coqPackages.contribs.Ssreflect -A coqPackages.contribs.MapleMode -A coqPackages.contribs.SquareMatrices -A coqPackages.contribs.Fermat4 -A coqPackages.contribs.TreeAutomata -A coqPackages.contribs.AACTactics -A coqPackages.contribs.Random -A coqPackages.contribs.IntMap -A coqPackages.contribs.Paradoxes -A coqPackages.contribs.Presburger -A coqPackages.contribs.String -A coqPackages.contribs.PTS -A coqPackages.contribs.GenericEnvironments -A coqPackages.contribs.IZF -A coqPackages.fiat -A coqPackages.contribs.CatsInZFC -A coqPackages.contribs.Matrices -A coqPackages.contribs.HighSchoolGeometry -A coqPackages.contribs.Checker -A coqPackages.contribs.Demos -A coqPackages.contribs.QArithSternBrocot -A coqPackages.tlc -A coqPackages.contribs.Fairisle -A coqPackages.contribs.ConstructiveGeometry -A coqPackages.contribs.SMC -A coqPackages.contribs.TreeDiameter -A coqPackages.contribs.ZChinese -A coqPackages.contribs.PersistentUnionFind -A coqPackages.contribs.ABP -A coqPackages.contribs.ZornsLemma -A coqPackages.contribs.Icharate -A coqPackages.contribs.ZSearchTrees -A coqPackages.contribs.Karatsuba -A coqPackages.contribs.LTL -A coqPackages.contribs.FOUnify -A coqPackages.contribs.CoqInCoq -A coqPackages.contribs.RulerCompassGeometry -A coqPackages.contribs.Nfix -A coqPackages.contribs.Multiplier -A coqPackages.contribs.CFGV -A coqPackages.contribs.Markov -A coqPackages.contribs.MathClasses -A coqPackages.contribs.Rational -A coqPackages.contribs.Hardware -A coqPackages.contribs.Buchberger -A coqPackages.contribs.LinAlg -A csdp -A coqPackages.contribs.CoLoR -A coqPackages.contribs.Additions -A coqPackages.contribs.Algebra -A coqPackages.contribs.Counting -A coqPackages_8_5.mathcomp -A coqPackages.contribs.GroupTheory -A coqPackages.contribs.CoinductiveExamples -A coqPackages.contribs.FSSecModel -A coqPackages.heq -A coqPackages.contribs.ConCaT -A coqPackages.contribs.PiCalc -A coqPackages.contribs.Dictionaries -A coqPackages.contribs.QuicksortComplexity -A coqPackages.contribs.DescenteInfinie -A coqPackages.contribs.AMM11262 -A coqPackages.contribs.PTSATR -A coqPackages.contribs.CoinductiveReals -A coqPackages.contribs.QArith -A coqPackages.contribs.SearchTrees -A coqPackages.contribs.SumOfTwoSquare -A coqPackages.contribs.Circuits -A coqPackages.contribs.ReflexiveFirstOrder -A coqPackages.contribs.FingerTree -A coqPackages.contribs.ATBR -A coqPackages.contribs.ZF -A coqPackages.contribs.Lambda -A coqPackages.contribs.Kildall -A coqPackages.coqeal -A coqPackages.contribs.lc -A coqPackages.ynot -A coqPackages.contribs.Goedel -A coqPackages.contribs.Stalmarck -A coqPackages.contribs.MiniC -A coqPackages.contribs.HigmanCF -A coqPackages.contribs.HistoricalExamples -A coqPackages.contribs.Prfx -A coqPackages.contribs.Bertrand -A coqPackages.contribs.Exceptions -A coqPackages.contribs.AxiomaticABP -A coqPackages.contribs.MiniCompiler -A coq_8_3 -A coqPackages.contribs.Rem -A coqPackages.contribs.JProver -A coqPackages.contribs.Automata -A coqPackages.contribs.ZFC -A coqPackages.contribs.Containers -A coqPackages.contribs.ClassicalRealizability -A coqPackages.contribs.Shuffle -A coqPackages.contribs.LesniewskiMereology -A coqPackages.contribs.Schroeder -A coqPackages.contribs.Graphs -A coqPackages.contribs.FSets -A coqPackages.contribs.HoareTut -A coqPackages.contribs.HigmanNW -A coqPackages.interval -A coqPackages.contribs.ThreeGap -A coqPackages.contribs.MutualExclusion -A coq_HEAD -A coqPackages.contribs.ReleasedSsreflect -A coqPackages.contribs.FundamentalArithmetics -A coqPackages.flocq -A coqPackages.contribs.FunctionsInZFC -A coqPackages.contribs.OtwayRees -A coqPackages.contribs.IdxAssoc -A coqPackages.contribs.FreeGroups -A coqPackages.contribs.Lambek -A coqPackages.contribs.lazyPCF -A coqPackages.contribs.PTSF -A coqPackages.contribs.AreaMethod -A coqPackages.contribs.Ergo -A coqPackages.mathcomp -A coqPackages.contribs.Cantor -A coqPackages.contribs.BDDs -A coqPackages.contribs.MiniML -A coqPackages.contribs.Float -A coqPackages.contribs.Coalgebras -A coqPackages.contribs.GC -A coqPackages.contribs.CCS -A coqPackages.contribs.EuclideanGeometry -A framac -A coqPackages_8_5.ssreflect -A coqPackages.contribs.OrbStab -A coqPackages.contribs.DistributedReferenceCounting -A coqPackages.contribs.Huffman -A coqPackages.contribs.ExactRealArithmetic -A coqPackages.contribs.Sudoku -A coqPackages.contribs.ProjectiveGeometry -A coqPackages.contribs.AILS -A coqPackages.contribs.Hedges -A coqPackages.contribs.Coqoban -A coqPackages.contribs.Tait -A coq -A coqPackages.contribs.Semantics -A coqPackages.contribs.JordanCurveTheorem -A coqPackages.contribs.ParamPi

[vbgl]

@roconnor: could this patch to coq be opt-in? As-is, it is opt-out: it can be disabled by setting the csdp argument of the coq derivation to null. I perceive it as a regression: without, the micromega tactic only work when csdp is installed, but this can be done through nix, or through the local system package manager, or by any other means, and independently. With this patch, csdp is turned into a build-time dependency, which looks wrong (indeed, coq does not need csdp to be built). Moreover, csdp does not currently build on darwin (because gfortran does not), and that breaks coq and what depends on it. Thanks.

[roconnor]

Soft dependencies are generally bad, so I prefer to keep it as is. To give an example, I really don't like the case where two people have the exact same version of coq, yet one person can check a given proof, but the other person cannot.

If csdp doesn't build on darwin, then you can patch the csdp derivation to return null on darwin systems.