deducteam / holide Goto Github PK
View Code? Open in Web Editor NEWA translator from OpenTheory to Dedukti
License: Other
holide's People
Contributors
Stargazers
Watchers
holide's Issues
quiet mode not quiet
Even with the option --quiet holide outputs "defineConstList defined here"
dkcheck doesn't seem to end on base-1.221
make install not compatible with opam
make install installs everything under /usr/local/bin and not in the opam directory.
error on list-replicate-1.62.art
holide ./packages/natural-def-1.29/natural-def-1.29.art ...Fatal error: exception Failure("type match: type operators bool and Number.Natural.natural do not agree")
dkcheck fails on relation-1.63
dkcheck relation-1.63.dk ...
[ERROR CODE:306] [relation-1.63.dk] [line:33420 column:1120]
Cannot find symbol 'relation-1.63.B'.
Failed test on `dedukti/relation.dko`: line:33420 column:1120 Cannot find symbol 'relation.B'.
ERROR line:33420 column:1120 Cannot find symbol 'relation.B'.
Makefile:184: recipe for target 'dedukti/relation.dko' failed
make[1]: *** [dedukti/relation.dko] Error 3
make[1]: Leaving directory '/home/travis/build/Deducteam/Holide'
See the Travis CI log for the full report:
- 4.02 version: https://travis-ci.org/Deducteam/Holide/jobs/607721715
- 4.09 version: https://travis-ci.org/Deducteam/Holide/jobs/607721722
configure: dkcheck called with wrong option
Hi. Following README.md, we just have to do make. But I get the following error on my machine:
07:03 ~/src/Holide (master) make
classic-display -libs str -I src -build-dir build main.native
bash: classic-display : commande introuvable
make: [Makefile:73 : holide] Erreur 127 (ignorée)
ln -sf build/src/main.native holide
cd dedukti/ && "/home/blanqui/.opam/4.11.1/bin/dkcheck" -e hol.dk
[SUCCESS] hol.dk was successfully checked.
Now, ./configure fails as well:
07:03 ~/src/Holide (master) ./configure
Looking for program 'dkcheck' in PATH.
Program 'dkcheck' found in PATH at "/home/blanqui/.opam/4.11.1/bin/dkcheck".
Asking 'dkcheck' for its version number.
Program 'dkcheck' has version '[Warning] [DEPRECATED] Flag -version is deprecated ! Use --version instead.
devel'.
./configure: ligne 22 : [: 2.6 : opérateur unaire attendu
ERROR: version constraint not satisfied: 2.6 <= [Warning] [DEPRECATED] Flag -version is deprecated ! Use --version instead.
devel
ERROR: version constraint not satisfied: [Warning] [DEPRECATED] Flag -version is deprecated ! Use --version instead.
devel = devel
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.