Closed mikolajpp closed 3 years ago
I hope our news docs will get a section on 'proving' stuff in practice. I have no idea where in the current docs I should turn for self-help, so it would be good to maybe add an article on two on such pitfalls.
Eh, I was hit again by https://github.com/urbit/arvo/issues/573
Yeah, and I think even if it were fixed you'd probably want to use a ?-
for clarity that you're matching on a $%
.
Hmm, why? I thought the purpose of ?:
was to be clear I am matching this for truth or false
which imo is much clearer than %&
, %|
...
?:
is just "if", and usually used in the context of ?: (gth foo bar)
etc.
If the conditional is specifically destructuring pattern-matching, with subject type implications, you want to use ?=
, ?-
, ?~
etc; which can frequently be ?: ?=(%| -.foo) ...early-return
in uneven-complexity cases.
OK, I see. Would it be possible to provide more information from the compiler in this case.
I am not taking about introducing more error messages, just a way to extract this information by clever code injection.
For example, in Plato I am gonna doing some tricks on nest-fail to get better error
Continued.
Better error messages by injecting debug code before offending expression to show their type.
So if it possible to somehow detect this error I would consider that a fix.
There's commented out "what did we want / what did we get" ~|s in the compiler/jets, if the type printer were less verbose those would probably be turned on by default :3
The proper way to make type printer less verbose would to make it stop at hoon types. All I want to know it tried to match against a tang, I don't care than that is a list of tanks which it then the union of… and so on.
How much work it would be to make it recognize fundamental types?
Or better yet, it should be aware of all types in current scope, including user defined ones. That's how compilers usually work.
The type printer is being massively overhauled as we speak :-)
On Sat, Apr 7, 2018 at 10:00 PM, mikolajpp notifications@github.com wrote:
Or better yet, it should be aware of all types in current scope, including user defined ones. That's how compilers usually work.
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/urbit/docs/issues/247#issuecomment-379520604, or mute the thread https://github.com/notifications/unsubscribe-auth/AALyAbla5O_qmiJ_56lTx3erWpsDYS1pks5tmZlmgaJpZM4TLKJO .
@cgyarvin This sounds too exciting...
I am able to get much more user friendlyness out of the current system in Plato than I thought (will release next week).
Essentially, I catch all types of errors I am able to get from tank printer. For syntax errors we mark the error line and put red glaring marks at the spot parser catched the cold.
For compiler errors we mark the offending fragment.
This in itself will be a huge upgrade from current peck hunting in the text editor. If type printer has coming upgrades, all the better!
Yeah, tanks are tanks because they are simple as hell and you can hack the hell them. There will be better ways to do all this.
I’m starting to actually want to use this thing of yours! Will it let me use vim (or at least neovim)?
Sent from my iPhone
On Apr 8, 2018, at 11:14 AM, mikolajpp notifications@github.com wrote:
@cgyarvin This sounds too exciting...
I am able to get much more user friendlyness out of the current system in Plato than I thought (will release next week).
Essentially, I catch all types of errors I am able to get from tank printer. For syntax errors we mark the error line and put red glaring marks at the spot parser catched the cold.
For compiler errors we mark the offending fragment.
This is itself will be a huge upgrade from current hunting in the text editor. If type printer has coming upgrades, all the better!
— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or mute the thread.
I presume you just want to use the Plato backend? Because for the frontend part, now we have only the original frontend, which works in the browser and uses ace editor (which I think has bindings of all major editors, including VIM).
That said, nothing prevents someone from hooking Plato itself into any editor. API is very simple, and I can get to document it next week.
Plato sur is this:
|%
+= job-type $? %parse
%compile
%invalid
==
+= job-status $?
%busy
%ok
%fail
==
+= error-kind $?
%syntax-error
%nest-fail
%mint-vain
%mint-lost
%find
%unknown
==
+= src-loc [row=@ud col=@ud]
+= job-error [loc=(list src-loc) kind=error-kind msg=tape]
+= job [type=job-type id=@ud stat=job-status src=tape blob=(unit hoon) err=(unit job-error) res=tape]
--
job is directly mapped to JSON.
The type printer cannot stop at "tried to match a type named tang
", as the current type type doesn't record the name of the arm that the mold that produced the type came from, but presumably that's part of the overhaul :P
@cgyarvin
The latest version of plato has error introspection working quite well:
We can surely talk about bringing this goodies to other editors, though I have never used neovim. All it needs is ability to make JSON HTTP requests to plato.
The information is there! Nice bandaid, but ++ut could still use a rewrite.
I've never worked with neovim -- I just have the vim bindings in my fingers, and I hear neovim is the only decent clone. Sadly, I can't make hacking this a priority for myself...
On Mon, Apr 9, 2018 at 12:37 PM, mikolajpp notifications@github.com wrote:
@cgyarvin https://github.com/cgyarvin
The latest version of plato has error introspection working quite well:
[image: sneak-peek] https://camo.githubusercontent.com/fdb058a9d6f3b07e6e5e553caaa09dba30ff034b/687474703a2f2f74696e79696d672e696f2f692f7664674b4b51612e676966
We can surely talk about bringing this goodies to other editors, though I have never used neovim. All it needs is ability to make JSON HTTP requests to plato.
— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/urbit/docs/issues/247#issuecomment-379869053, or mute the thread https://github.com/notifications/unsubscribe-auth/AALyAY2V6yQuPPl_md4Dv9mfPBHj9Wsdks5tm7hcgaJpZM4TLKJO .
@cgyarvin , I would very much prefer ++ut having a rewrite.
Plato has inflated to 400 lines half of which is re-parsing of errors.
So what's the editor you are using right now? It would be cool for plato to gain another frontend - provided it is possible to hook whatever you are using right into plato via HTTP requests
Stock vim, sounds like. Which can maybe have a Plato highlighting layer hacked into it with scripts?
Do not under any circumstances do any engineering on or near stock vim. I can certainly switch to neovim. :-)
Sent from my iPhone
On Apr 10, 2018, at 8:40 AM, Anton Dyudin notifications@github.com wrote:
Stock vim, sounds like. Which can maybe have a Plato highlighting layer hacked into it with scripts?
— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or mute the thread.
Haven't you heard? Vimscript is an excellent language with many features :) :) :)
On Tuesday, 10 April 2018, cgyarvin notifications@github.com wrote:
Do not under any circumstances do any engineering on or near stock vim. I can certainly switch to neovim. :-)
Sent from my iPhone
On Apr 10, 2018, at 8:40 AM, Anton Dyudin notifications@github.com wrote:
Stock vim, sounds like. Which can maybe have a Plato highlighting layer hacked into it with scripts?
— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or mute the thread.
— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/urbit/docs/issues/247#issuecomment-380158826, or mute the thread https://github.com/notifications/unsubscribe-auth/ABxXhigGY92i6JBVwMhm_0tFKZdaIzaOks5tnNnsgaJpZM4TLKJO .
It seems dabbling at frontend for far too long and I forgot some crucial parts of Hoon. We have this little snippet (best used wit plato!):
I know that in case of parser failure p.a is a list of tanks (a tang). But it seems compiler knows better. No matter how many checks I put in, it always fails with nest-fail. I am correctly dispatching on failure flag with
?:
. Then prove that list is non-empty with?~
. What is missing?