search

codewars / codewars-runner-cli

Old CodeRunner project. See https://github.com/codewars/runner instead.
GNU Affero General Public License v3.0
402 stars 141 forks source link

`Load` doesn't work like `Require` in Coq #756

Closed Voileexperiments closed 5 years ago

Voileexperiments commented 5 years ago

In a local Coq installation, running

Print Libraries.
Load Bool.
Print Libraries.

Gives

Loaded and imported library files: 
  Coq.Init.Notations
  Coq.Init.Logic
  Coq.Init.Logic_Type
  Coq.Init.Datatypes
  Coq.Init.Specif
  Coq.Init.Peano
  Coq.Init.Wf
  Coq.Init.Tactics
  Coq.Init.Tauto
  Coq.Init.Prelude

Loaded and not imported library files: 
  Coq.Init.Decimal
  Coq.Init.Nat

Bool.v has been found in
[ C:\Coq\lib\coq\user-contrib\ExtLib\Data ; C:\Coq\lib\coq\theories\Bool ];
loading C:\Coq\lib\coq\user-contrib\ExtLib\Data\Bool.v [ambiguous-file-name,filesystem]
Loaded and imported library files: 
  Coq.Init.Notations
  Coq.Init.Logic
  Coq.Init.Logic_Type
  Coq.Init.Datatypes
  Coq.Init.Specif
  Coq.Init.Peano
  Coq.Init.Wf
  Coq.Init.Tactics
  Coq.Init.Tauto
  Coq.Init.Prelude
  ExtLib.Core.RelDec

Loaded and not imported library files: 
  Coq.Init.Decimal
  Coq.Init.Nat
  Coq.Bool.Bool
  Coq.Program.Basics
  Coq.Classes.Init
  Coq.Program.Tactics
  Coq.Relations.Relation_Definitions
  Coq.Classes.RelationClasses
  Coq.Classes.CRelationClasses
  Coq.Classes.CMorphisms
  Coq.Classes.Morphisms
  Coq.Classes.Morphisms_Prop
  Coq.Classes.Equivalence
  Coq.Classes.SetoidTactics
  Coq.Setoids.Setoid

And then things from Coq.Bool.Bool can be used under Bool.

However, on CW runner this happens:

Loaded and imported library files: 
  Coq.Init.Notations
  Coq.Init.Logic
  Coq.Init.Logic_Type
  Coq.Init.Datatypes
  Coq.Init.Specif
  Coq.Init.Peano
  Coq.Init.Wf
  Coq.Init.Tactics
  Coq.Init.Tauto
  Coq.Init.Prelude

Loaded and not imported library files: 
  Coq.Init.Decimal
  Coq.Init.Nat

Loaded and imported library files: 
  Coq.Init.Notations
  Coq.Init.Logic
  Coq.Init.Logic_Type
  Coq.Init.Datatypes
  Coq.Init.Specif
  Coq.Init.Peano
  Coq.Init.Wf
  Coq.Init.Tactics
  Coq.Init.Tauto
  Coq.Init.Prelude

Loaded and not imported library files: 
  Coq.Init.Decimal
  Coq.Init.Nat

And things under Bool is not loaded. However the command Load Bool doesn't fail (if Bool is not at the loadpath it should fail with Can't find file Bool.v on loadpath instead), so clearly something weird is happening with the CW runner loadpath setup.

(Require works as intended, of course.)

kazk commented 5 years ago

So the difference is

+List.v has been found in
+[ C:\Coq\lib\coq\user-contrib\Mtac2\lib ;
+  C:\Coq\lib\coq\user-contrib\ExtLib\Data ;
+  C:\Coq\lib\coq\theories\Lists ];
+loading C:\Coq\lib\coq\user-contrib\Mtac2\lib\List.v [ambiguous-file-name,filesystem]

+  Mtac2.lib.Datatypes

?

Do you know if there's any difference between Windows and Linux? On my machine, the output is the same as the runner.

The runner just does coqc Solution.v. Is there a way to check the loadpath?

Voileexperiments commented 5 years ago

Oops, I just realized that the output I posted is for Load List. I just fixed the output. The same thing happens with List and other things though.

Yes, I'm using a Windows installation, stepping through Coq files in CoqIde in interactive mode. Does it make a difference from just using coqc?

kazk commented 5 years ago

For Load Bool.. Your output has

Bool.v has been found in
[ C:\Coq\lib\coq\user-contrib\ExtLib\Data ; C:\Coq\lib\coq\theories\Bool ];
loading C:\Coq\lib\coq\user-contrib\ExtLib\Data\Bool.v [ambiguous-file-name,filesystem]

For the runner, coq/user-contrib/ExtLib/Data/Bool.v doesn't exist, but coq/theories/Bool/Bool.v does.

For Load List.. The runner's output is

Loaded and imported library files: 
  Coq.Init.Notations
  Coq.Init.Logic
  Coq.Init.Logic_Type
  Coq.Init.Datatypes
  Coq.Init.Specif
  Coq.Init.Peano
  Coq.Init.Wf
  Coq.Init.Tactics
  Coq.Init.Tauto
  Coq.Init.Prelude

Loaded and not imported library files: 
  Coq.Init.Decimal
  Coq.Init.Nat

Loaded and imported library files: 
  Coq.Init.Notations
  Coq.Init.Logic
  Coq.Init.Logic_Type
  Coq.Init.Datatypes
  Coq.Init.Specif
  Coq.Init.Peano
  Coq.Init.Wf
  Coq.Init.Tactics
  Coq.Init.Tauto
  Coq.Init.Prelude
  Coq.Arith.PeanoNat
  Coq.Arith.Le
  Coq.Arith.Gt
  Coq.Arith.Minus
  Coq.Bool.Bool
  Coq.Arith.Lt

Loaded and not imported library files: 
  Coq.Init.Decimal
  Coq.Init.Nat
  Coq.Program.Basics
  Coq.Classes.Init
  Coq.Program.Tactics
  Coq.Classes.CRelationClasses
  Coq.Relations.Relation_Definitions
  Coq.Classes.CMorphisms
  Coq.Classes.RelationClasses
  Coq.Classes.Morphisms
  Coq.Classes.Morphisms_Prop
  Coq.Classes.Equivalence
  Coq.Classes.SetoidTactics
  Coq.Setoids.Setoid
  Coq.Structures.Equalities
  Coq.Relations.Relation_Operators
  Coq.Relations.Operators_Properties
  Coq.Relations.Relations
  Coq.Structures.Orders
  Coq.Numbers.NumPrelude
  Coq.Structures.OrdersTac
  Coq.Structures.OrdersFacts
  Coq.Structures.GenericMinMax
  Coq.Numbers.NatInt.NZAxioms
  Coq.Numbers.NatInt.NZBase
  Coq.Numbers.NatInt.NZAdd
  Coq.Numbers.NatInt.NZMul
  Coq.Logic.Decidable
  Coq.Numbers.NatInt.NZOrder
  Coq.Numbers.NatInt.NZAddOrder
  Coq.Numbers.NatInt.NZMulOrder
  Coq.Numbers.NatInt.NZParity
  Coq.Numbers.NatInt.NZPow
  Coq.Numbers.NatInt.NZSqrt
  Coq.Numbers.NatInt.NZLog
  Coq.Numbers.NatInt.NZDiv
  Coq.Numbers.NatInt.NZGcd
  Coq.Numbers.NatInt.NZBits
  Coq.Numbers.Natural.Abstract.NAxioms
  Coq.Numbers.NatInt.NZProperties
  Coq.Numbers.Natural.Abstract.NBase
  Coq.Numbers.Natural.Abstract.NAdd
  Coq.Numbers.Natural.Abstract.NOrder
  Coq.Numbers.Natural.Abstract.NAddOrder
  Coq.Numbers.Natural.Abstract.NMulOrder
  Coq.Numbers.Natural.Abstract.NSub
  Coq.Numbers.Natural.Abstract.NMaxMin
  Coq.Numbers.Natural.Abstract.NParity
  Coq.Numbers.Natural.Abstract.NPow
  Coq.Numbers.Natural.Abstract.NSqrt
  Coq.Numbers.Natural.Abstract.NLog
  Coq.Numbers.Natural.Abstract.NDiv
  Coq.Numbers.Natural.Abstract.NGcd
  Coq.Numbers.Natural.Abstract.NLcm
  Coq.Numbers.Natural.Abstract.NBits
  Coq.Numbers.Natural.Abstract.NProperties
  Coq.Arith.Plus

coq/user-contrib/Mtac2 or coq/user-contrib/ExtLib doesn't exist, but coq/theories/Lists/List.v exists. (This output includes Coq.Bool.Bool :/)

I guess your setup have more libraries installed and it's loading different file from the runner. has been found in [ ...]; loading ... [ambiguous-file-name,filesystem].

However the command Load Bool doesn't fail (if Bool is not at the loadpath it should fail with Can't find file Bool.v on loadpath instead), so clearly something weird is happening with the CW runner loadpath setup.

I think it doesn't fail because Bool.v and List.v are found and loaded. It's just not loading the same file as yours.

kazk commented 5 years ago

Can you try loading a file (C:\Coq\lib\coq\theories\Bool\Bool.v) and see if it behaves like the runner?

Print Libraries.
Load "C:\Coq\lib\coq\theories\Bool\Bool.v".
Print Libraries.
kazk commented 5 years ago

From the documentation, Load and Require does different things. And the output looks like it's working as expected to me (just loading different files from yours), but I don't know Coq.

@monadius, @Bubbler-4, @DonaldKellett any idea?

Voileexperiments commented 5 years ago

https://github.com/coq/coq/wiki/Installation-of-Coq-on-Windows

Apparently additional packages are bundled in the windows installer:

The installer also includes precompiled .vo files for the standard library. Since version 8.8, this installer also includes the possibility to install additional Coq packages. The installers for 8.8.2 and later includes these packages:

aactactics, bignums, compcert, coquelicot, equations, extlib, ltac2, mathcomp, menhir, menhirlib, mtac2, quickchick, vst

Voileexperiments commented 5 years ago

Can you try loading a file (C:\Coq\lib\coq\theories\Bool\Bool.v) and see if it behaves like the runner?

I just did, the end result was the same as the runner.

Bubbler-4 commented 5 years ago

IMHO this sounds like a non-issue. It's just a thing that matters only in the golfing context (no one will Load a module for a regular task) and only in a not-so-well-designed golfing challenge (where the standard library can trivially solve it).

kazk commented 5 years ago

Closing as not an issue.