Comments (4)
lsf37
commented on September 23, 2024
It should be reasonably easy to update to newer GHC versions, and it's probably a about time that we do that. Unless you're already planning to submit a pull request for this one, I'll put it on our TODO list.
from l4v.
lsf37
commented on September 23, 2024
(ps: the thread you reference also has a (somewhat distasteful) workaround)
from l4v.
yanok
commented on September 23, 2024
I've made a PR fixing this issue. BTW, is your TODO list publicly available somewhere?
from l4v.
lsf37
commented on September 23, 2024
Saw that - test is running. The TODO list (main issue tracker) is currently internal only -- too much entanglement with other projects and customer projects for now to easily make it public. I've been thinking about automated mirroring of a subset to github or things like that, but all options seem complicated.
from l4v.
Related Issues (20)
- should `corres_cases` also do case distinction on `if`?
- Cannot load theory file "l4v/proof/crefine/autocorres-test/Refine_C.thy" HOT 4
- Investigate adding `projectKOs` to the simp set HOT 1
- Remove instances of `UNIV <\inter>` from CRefine
- Cleanup CRefine Wellformed_C
- Cleanup post-x64 comments
- Document mysterious useful comments for ctac and ceqv
- SIMPL: don't print `_'proc`
- CI artifact upload uses clashing artifact names
- Methods such as monadic_rewrite_symb_exec_r should warn that discharging side-conditions failed
- Safer vcg in CRefine
- Sub-term to free variable lifting tactic
- Have wp warn when resulting in a goal with a schematic assumption. HOT 15
- Some way of blocking `simp` from unifying schematics HOT 1
- Decide on style for `[def]rule_tac ... [and ...] in ...` HOT 7
- Investigate further use of `none_top/none_bot` in the proofs
- Enhance C Parser to allow named array bounds HOT 3
- Can Isabelle's custom functions and data types be combined with the C-parser?
- take L4V_PLAT into account in rebuilds
- support strongest-postcondition reasoning HOT 1
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 l4v.