0dyl
Joined 5 years ago
Karma
160
Submissions
33
Member since
Jun 1
Author of the article "Driving with D"
View on Hacker NewsRecent submissions
Comment · 11 months ago
The new TI C2000 F29 series of microcontrollers are VLIW
Comment · 1 year ago
My apologies for getting frustrated. I shouldn’t have done that.
This is bit on info-dump. I’m not the best at expressing myself and so some parts may not be clear. Please feel free to ask for clarification or any further questions.
Pattern matching is available as a language extension (currently) exclusive to GNAT GCC. It’s not in the reference manual, which means it’s not part of standardised Ada (yet). It’s intended to be an experiment or prototype for what will eventually become a standardised language feature (the standardised feature may be different, or it could be rejected, as the standardisation committee is composed of multiple compiler vendors).
As is, that pattern matching feature works in both normal Ada and in SPARK mode on GNAT GCC 15.2. The flag to enable it is “-gnatX0”. Please see these: https://godbolt.org/z/d55ddznfn https://gcc.gnu.org/onlinedocs/gnat_rm/Case-pattern-matching... https://gcc.gnu.org/onlinedocs/gcc-15.1.0/gnat_rm/How-to-act... In the Godbolt example, that is in normal Ada.
You are not alone in finding the Ada community difficult to navigate. The “ada-spark-rfcs” repository you linked is a community outreach program of AdaCore to solicit feedback from programmers in venues they’re more likely to use. Those RFCs are then forwarded to the Ada Rapporteurs Group (ARG) who focus on the development of standardised Ada. Their issues, mailing list and meeting minutes can be found at: http://www.ada-auth.org/arg.html
SPARK doesn’t add features to Ada; instead, it’s a subset of features that can be easily proven by SMTs for formal verification. The special things in SPARK (extra attributes and pragmas, which Ada implementations are allowed to define) are only to aid formal verification. When language features are added, they’re added to Ada first and subsequently potentially enabled in SPARK.
I admit that calling it “ada-spark-rfcs” is kinda confusing - it’s just dumping ground for ideas for Ada and SPARK. For example, the multiple ghost levels RFC really only applies to SPARK, as ghost code only exists to improve verifiability. The final modifier RFC is for Ada proper, and it’ll probably apply to SPARK as it allows OOP.
The situation regarding compiler available is confusing and it made me nervous when I was first learning about the language.
GNAT GCC has two versions: FSF and PRO. The FSF (as in the Free Software Foundation) version is the publicly available version that’s in mainline GCC. PRO is for paying customers of AdaCore. From what I can tell, it’s built against an older version of the GCC backend. It tends to get those newest experimental features sooner, but they do trickle into FSF GCC. There have been points in time where I haven’t noticed any difference in feature set between GNAT PRO (according to the release notes) and those in FSF.
SPARK code works with both GNAT FSF and GNAT PRO. The formal verification tool for SPARK, GNATprove, is open source. https://github.com/AdaCore/spark2014
Have a great day. :)
Edit: I’m not affiliated with AdaCore. I’ve never even spoken to one of their employees on the forums. I do use Ada, but only in my “side-business” (not making any money yet lol).
Comment · 1 year ago
>Ada has a neglected dialect and a proprietary dialect
What on earth are you on about? That’s not the case.
Ada 2022 has been released and Ada 202x is getting improvements. Those features are trickling into FSF GNAT (GCC).
Are you talking about the SPARK dialect, where GNATprove is open source?
Comment · 5 years ago
> we genuinely can only laugh at people
That's perhaps not the best wording.
Nonetheless, I do agree with you. D can be very flexible in that regard.
Comment · 5 years ago
I'll try to get some website up in the future!
Comment · 5 years ago
It's very much the same in Australia.
The approval I got from the engineer was due to the following points:
1. The 6 speed came out of a newer generation of the model.
2. My controller has some safety features.
3. My controller emulates factory hydraulic behaviour. Had I implemented something like a transbrake, I would have been in for a very long ride of red tape.
Comment · 5 years ago
That really sucks :(
Comment · 5 years ago
If my car relied heavily on CAN (like the next generation Commodore) I probably would have sold it.
I love CAN bus (for my own designs), but I don't see the effort of attempting to reverse engineer GM's format as worth it, especially since I had no prior experience with CAN.
Thank you :) I've got another D automotive project which I hope to write about soon.
Comment · 5 years ago
Thank you!
I agree, the syntax is much clearer than C++. The very first prototype was in C++, but I found myself frequently frustrated with the language. I find D's features make me more productive.
Comment · 5 years ago
As of current, no. I'm not sure where I want to go with this project.
Comment · 5 years ago
Definitely. If you come from a C-family background it feels quite familiar.
Comment · 5 years ago
I was quite surprised, too. Maybe it was a little gift from Holden to the burnout bogans?
1. My apologies, I've confused you. CAN communications are purely internal for my system, it doesn't communicate via CAN to the car's computers.
The sensors and actuators give or accept voltage signals, and my controller inputs or outputs those accordingly. For example, the 4 speed has some pressure sensors to monitor the valve body behaviour, and I send some HI or LO voltage signals in emulation of it.
2. I do use FreeRTOS for the 407. I don't need to, since I use a super loop and all my memory is either static or allocated on the stack.
Comment · 5 years ago
I plan to keep it for a while yet!