Obnoxious error in build/gen_stub.php "PHPDoc param type is unnecessary"

[dktapps]

Description

build/gen_stub.php bails out if it encounters doc comments like this:

     * @param int $size The maximum number of Workers this Pool can create
     * @param string $class The class for new Workers
     * @param array $ctor An array of arguments to be passed to new Workers

complaining that the @param annotations are unnecessary. It's my opinion that bailing out here is entirely unnecessary and annoying. A warning would be perfectly sufficient.
In addition, it makes it inconvenient to write doc comments in stubs.

[damianwadley]

It's correct in that saying the parameter is a string is redundant, the problem is that it's not accounting for the fact that there's a description too. So IMO it should "error" if you say like @param string $class and nothing else, obviously allow @param string $class description here, then the error message should say that either you remove the tag or you add a description.

[dktapps]

Yeah, the description part is fair enough. But I don't believe this should be a fatal error at all. I simply removed the check on my local because I was repurposing old stubs for header generation and didn't want to remove all the comments.

[nikic]

I think it's fine to just drop the check. For php-src usage we don't include docs in stubs, but it's reasonable that extensions want to do this, and I don't think this check is preventing any real bugs.

cc @kocsismate

[cmb69]

I think it's fine to just drop the check.

I agree, but we may consider to add check for a doc-type not matching the declared type (might be too complex, though), since this is a more serious issue anyway.

[kocsismate]

@nikic Yes, you are right, the check is not really useful.

I agree, but we may consider to add check for a doc-type not matching the declared type (might be too complex, though), since this is a more serious issue anyway.

The idea is great, but implementing this would take way too much time (for me at least), so I'd spare my time for something else.