Comments (4)
Tests that use test_wholefile.v
have been disabled in a6ec628.
from pg.
Hi @hendriktews, good catch;
but IINM, the test_wholefile.v
was intended to test PG capabilities on a realistic Coq example.
It appears the test file rusted, but maybe a better solution would be to adapt the test script, not to disable it?
WDYT?
from pg.
Yes, polishing the Coq code to get the test running again would indeed be better. I had to adapt the test twice in the past. Seeing it now failing again because of a deprecated feature after nobody had reacted to #698 and seeing that the code is far below my coding standards (no indentation, no proof using,...) I was not motivated to touch it again. I would certainly appreciate if somebody takes care of test_wholefile.v
, although I believe we have more urgent problems to address in PG.
from pg.
Seeing it now failing again because of a deprecated feature after nobody had reacted to #698
Yes, sorry 😅
and seeing that the code is far below my coding standards (no indentation, no proof using,...)
Actually, that file was just a theory from coq's stdlib - which does not impose as many coding conventions as, for example, ssreflect/mathcomp theories.
I was not motivated to touch it again. I would certainly appreciate if somebody takes care of test_wholefile.v, although I believe we have more urgent problems to address in PG.
Sure! no worries to keep the test as is for now! and I'll remember the task so I could address it in a couple of weeks.
BTW if I might help a bit at the beginning of next week, which issue/PR would be the more urgent from your viewpoint?
from pg.
Related Issues (20)
- makeinfo reports warning: @inforef is obsolete
- compile-tests/003-require-error fails sporadically with 8.19-rc1 HOT 4
- Build failure when "Compile Before Require" meets imported OCaml plugins HOT 13
- proof-goto-point is non-idempotent HOT 2
- wait for proof-goto-point to finish HOT 1
- void function error
- coq-load-project file should extract META files HOT 1
- dynamic highlighting HOT 1
- Bug: Frames in hybrid mode automatically revert to vertical mode HOT 2
- different styles of comment HOT 6
- Indentation issue : "\in" HOT 2
- 3-pane mode broken with small frame heights
- UI and kernel out of sync from aborting tactics? HOT 1
- Proof General gets into a state where it doesn't know what + is. HOT 11
- Why retracting before restarting coqtop? HOT 3
- Incompatibility with `package-quickstart` HOT 4
- bug: newlines misparsed as space in string litterals HOT 10
- File mode specification error: (void-variable coq-cmd-force-next-proof-kept) HOT 14
- REGRESSION: ProofGeneral cannot step over Fail correctly HOT 10
- PG does not position to error HOT 8
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.
from pg.