search

idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.43k stars 643 forks source link

--partial-eval and --no-partial-eval arguments are accepted at once #2207

Open osa1 opened 9 years ago

osa1 commented 9 years ago

It seems to me like --no-partial-eval and --partial-eval should be merged and converted to a switch instead of separate flags. This way we can set it False by default, and True when --no-partial-eval is passed.

Here's what happens in HEAD:

➜   idris --partial-eval --no-partial-eval
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 0.9.17.1-git:e7f9257
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help               

Idris is free software with ABSOLUTELY NO WARRANTY.            
For details type :warranty.
Idris>

Accepted without any warnings or errors. I have no ideas whether partial evaluation is enabled or disabled.

osa1 commented 9 years ago

I'm moving IRC discussion to here:

Apparently this is deliberately done, what should happen is that last argument should be the valid one. (make sure this is working)